Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
From MaRDI portal
Publication:5049005
DOI10.1007/978-3-030-51054-1_14OpenAlexW3039465858MaRDI QIDQ5049005FDOQ5049005
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
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
- Extending Sledgehammer with SMT Solvers
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Title not available (Why is that?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Lattices and ordered algebraic structures
- Title not available (Why is that?)
- Title not available (Why is that?)
- Constructions of p-algebras
- Locales: a module system for mathematical theories
- On sentences which are true of direct unions of algebras
- Die Kennzeichnung der distributiven pseudokomplementären Halbverbände.
- Rough sets. Mathematical foundations
- Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
- Constructive Type Classes in Isabelle
- Stone Lattices. I: Construction Theorems
- An algebraic framework for minimum spanning tree problems
- Implicative Semi-Lattices
- Title not available (Why is that?)
- Title not available (Why is that?)
- A New Proof of the Construction Theorem for Stone Algebras
- Verifying minimum spanning tree algorithms with Stone relation algebras
- Title not available (Why is that?)
- Type classes for mathematics in type theory
- From types to sets by local type definition in higher-order logic
- Title not available (Why is that?)
Cited In (1)
Uses Software
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)
