Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
From MaRDI portal
Recommendations
- Automating free logic in Isabelle/HOL
- Frontiers of Combining Systems
- Automatic proof and disproof in Isabelle/HOL
- Isabelle/UTP: a mechanised theory engineering framework
- Isabelle/HOL. A proof assistant for higher-order logic
- The formal derivation of algorithm and automatic verification based on Isabelle
- Building Formal Method Tools in the Isabelle/Isar Framework
- On Automating the Calculus of Relations
- scientific article; zbMATH DE number 1670741
Cited in
(18)- Cryptomorphic topological structures: a computational, relation-algebraic approach
- Left omega algebras and regular equations
- In praise of algebra
- Relational characterisations of paths
- Leveraging the information contained in theory presentations
- Modelling algebraic structures and morphisms in ACL2
- Using relation-algebraic means and tool support for investigating and computing bipartitions
- Isabelle/UTP: a mechanised theory engineering framework
- Automated Reasoning in Higher-Order Regular Algebra
- On completeness of omega-regular algebras
- Unifying heterogeneous state-spaces with lenses
- Defense in Depth Formulation and Usage in Dynamic Access Control
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- Completeness for identity-free Kleene lattices
- Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
- RALL: machine-supported proofs for relation algebra
- Artificial Intelligence and Symbolic Computation
- Cardinality of relations with applications
This page was built for publication: Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3007567)
