Automated Reasoning in Higher-Order Regular Algebra

DOI10.1007/978-3-642-33314-9_5MaRDI QIDQ2915136zbMATH OpenOpenAlexFDO

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) Quantales (06F07) Algebraic theory of languages and automata (68Q70)

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

• 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 analysis of regular algebra
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• Automatic proof and disproof in Isabelle/HOL
• Hints in Unification
• 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?)
• 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)

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

Describes a project that uses

Uses Software

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

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)