Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL

DOI10.1007/978-3-030-51054-1_14OpenAlexW3039465858MaRDI QIDQ5049005

Walter Guttmann

Publication date: 9 November 2022

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-51054-1_14

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Isabelle/HOL
• Sledgehammer
• Locales
• Transfer
• Lifting
• Archive Formal Proofs

Cites Work

• Constructions of p-algebras
• Isabelle/HOL. A proof assistant for higher-order logic
• From types to sets by local type definition in higher-order logic
• Lattices and ordered algebraic structures
• An algebraic framework for minimum spanning tree problems
• Rough sets. Mathematical foundations
• Verifying minimum spanning tree algorithms with Stone relation algebras
• Locales: a module system for mathematical theories
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• Type classes for mathematics in type theory
• Constructive Type Classes in Isabelle
• Extending Sledgehammer with SMT Solvers
• Implicative Semi-Lattices
• Stone Lattices. I: Construction Theorems
• Die Kennzeichnung der distributiven pseudokomplementären Halbverbände.
• A New Proof of the Construction Theorem for Stone Algebras
• On sentences which are true of direct unions of algebras
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL