Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL

DOI10.1007/978-3-030-51054-1_14MaRDI QIDQ5049005OpenAlexFDO

Authors 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)

Recommendations

• scientific article; zbMATH DE number 2110621
• scientific article; zbMATH DE number 2003161
• Algebras for program correctness in Isabelle/HOL
• Formalizing implicative algebras in Coq
• Higher-order separation logic in Isabelle/HOLCF
• Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• Equational reasoning in Isabelle
• Theorem Proving in Higher Order Logics
• A consistent foundation for Isabelle/HOL

Cites work

• scientific article; zbMATH DE number 3150853 (Why is no real title available?)
• scientific article; zbMATH DE number 3907750 (Why is no real title available?)
• scientific article; zbMATH DE number 3751028 (Why is no real title available?)
• scientific article; zbMATH DE number 3787631 (Why is no real title available?)
• scientific article; zbMATH DE number 3501559 (Why is no real title available?)
• scientific article; zbMATH DE number 1748069 (Why is no real title available?)
• scientific article; zbMATH DE number 1420790 (Why is no real title available?)
• scientific article; zbMATH DE number 1424016 (Why is no real title available?)
• scientific article; zbMATH DE number 3245483 (Why is no real title available?)
• scientific article; zbMATH DE number 3366941 (Why is no real title available?)
• A New Proof of the Construction Theorem for Stone Algebras
• An algebraic framework for minimum spanning tree problems
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• Constructions of p-algebras
• Constructive Type Classes in Isabelle
• Die Kennzeichnung der distributiven pseudokomplementären Halbverbände.
• Extending Sledgehammer with SMT solvers
• From types to sets by local type definition in higher-order logic
• Implicative Semi-Lattices
• Isabelle/HOL. A proof assistant for higher-order logic
• Lattices and ordered algebraic structures
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Locales: a module system for mathematical theories
• On sentences which are true of direct unions of algebras
• Rough sets. Mathematical foundations
• Stone Lattices. I: Construction Theorems
• Type classes for mathematics in type theory
• Verifying minimum spanning tree algorithms with Stone relation algebras

Cited in

(1)

• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5049005)