Automated Reasoning in Higher-Order Regular Algebra
DOI10.1007/978-3-642-33314-9_5zbMATH Open1364.68326OpenAlexW202642932MaRDI QIDQ2915136FDOQ2915136
Authors: Alasdair Armstrong, Georg Struth 
Publication date: 21 September 2012
Published in: Relational and Algebraic Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-33314-9_5
Recommendations
- Automated Reasoning in Kleene Algebra
- Automated analysis of regular algebra
- scientific article; zbMATH DE number 978243
- scientific article; zbMATH DE number 1303628
- scientific article; zbMATH DE number 1552534
- scientific article; zbMATH DE number 1185498
- Automated deduction in ring theory
- AUTOMATED COMPOSITIONAL REASONING OF INTUITIONISTICALLY CLOSED REGULAR PROPERTIES
- Automated Compositional Reasoning of Intuitionistically Closed Regular Properties
- Automated reasoning in some local exensions of ordered structures
Galois correspondences, closure operators (in relation to ordered sets) (06A15) Algebraic theory of languages and automata (68Q70) Quantales (06F07)
Cites Work
- Automatic proof and disproof in Isabelle/HOL
- A calculational approach to mathematical induction
- Title not available (Why is that?)
- Two Complete Axiom Systems for the Algebra of Regular Events
- Automated analysis of regular algebra
- A completeness theorem for Kleene algebras and the algebra of regular events
- Une remarque sur les systèmes complets d'identités rationnelles
- Title not available (Why is that?)
- Une condition impliquant toutes les identités rationnelles
- Internal axioms for domain semirings
- Title not available (Why is that?)
- Packaging Mathematical Structures
- Proof Pearl: regular expression equivalence and relation algebra
- Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
- An efficient Coq tactic for deciding Kleene algebras
- Local Theory Specifications in Isabelle/Isar
- Hints in Unification
- A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
- Left omega algebras and regular equations
Cited In (6)
- Title not available (Why is that?)
- On the fine-structure of regular algebra
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- Developments in concurrent Kleene algebra
- Building program construction and verification tools from algebraic principles
- Automated analysis of regular algebra
Uses Software
This page was built for publication: Automated Reasoning in Higher-Order Regular Algebra
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2915136)
