Automated Reasoning in Higher-Order Regular Algebra

DOI10.1007/978-3-642-33314-9_5MaRDI QIDQ2915136zbMATHOpenAlexFDO

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

Mathematics Subject Classification ID

Galois correspondences, closure operators (in relation to ordered sets) (06A15) Algebraic theory of languages and automata (68Q70) Quantales (06F07)

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

Cites work

• scientific article; zbMATH DE number 4210141 (Why is no real title available?)
• scientific article; zbMATH DE number 549971 (Why is no real title available?)
• scientific article; zbMATH DE number 3366846 (Why is no real title available?)
• A calculational approach to mathematical induction
• A completeness theorem for Kleene algebras and the algebra of regular events
• A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
• An efficient Coq tactic for deciding Kleene algebras
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• Automated analysis of regular algebra
• Automatic proof and disproof in Isabelle/HOL
• Hints in Unification
• Internal axioms for domain semirings
• Left omega algebras and regular equations
• Local Theory Specifications in Isabelle/Isar
• Packaging Mathematical Structures
• Proof Pearl: regular expression equivalence and relation algebra
• Two Complete Axiom Systems for the Algebra of Regular Events
• Une condition impliquant toutes les identités rationnelles
• Une remarque sur les systèmes complets d'identités rationnelles

Cited in

(6)

• Automated analysis of regular algebra
• Building program construction and verification tools from algebraic principles
• On the fine-structure of regular algebra
• Automated Algebraic Reasoning for Collections and Local Variables with Lenses
• scientific article; zbMATH DE number 978243 (Why is no real title available?)
• Developments in concurrent Kleene algebra

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL
• Isabelle/Isar
• Sledgehammer
• Myhill-Nerode
• Archive Formal Proofs
• Regular Sets
• Worker/Wrapper Transformation

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)