Automated Reasoning in Higher-Order Regular Algebra

DOI10.1007/978-3-642-33314-9_5zbMath1364.68326OpenAlexW202642932MaRDI QIDQ2915136

Georg Struth, Alasdair Armstrong

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

Related Items (2)

Developments in concurrent Kleene algebra ⋮ Building program construction and verification tools from algebraic principles

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Internal axioms for domain semirings
• A completeness theorem for Kleene algebras and the algebra of regular events
• A calculational approach to mathematical induction
• Left omega algebras and regular equations
• Proof Pearl: regular expression equivalence and relation algebra
• Automated Analysis of Regular Algebra
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
• Automatic Proof and Disproof in Isabelle/HOL
• Hints in Unification
• Packaging Mathematical Structures
• Une remarque sur les systèmes complets d'identités rationnelles
• Local Theory Specifications in Isabelle/Isar
• Une condition impliquant toutes les identités rationnelles
• Two Complete Axiom Systems for the Algebra of Regular Events
• An Efficient Coq Tactic for Deciding Kleene Algebras

This page was built for publication: Automated Reasoning in Higher-Order Regular Algebra