On the fine-structure of regular algebra

DOI10.1007/s10817-014-9318-9zbMath1331.68128MaRDI QIDQ2352506

Georg Struth, Simon Foster

Publication date: 2 July 2015

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://eprints.whiterose.ac.uk/103045/1/regalg.pdf

zbMATH Keywords

regular languages; automated theorem proving; interactive theorem proving; Kleene algebra; formalised mathematics; regular algebra

Mathematics Subject Classification ID

68Q45: Formal languages and automata

68Q70: Algebraic theory of languages and automata

Related Items

Regular_Algebras

Uses Software

• ACL2
• LEO-II
• Nitpick
• Isabelle/HOL
• Sledgehammer
• Transfer
• Lifting
• Myhill-Nerode
• Archive Formal Proofs
• Kleene Algebra
• Regex_Equivalence

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algebraic notions of nontermination: Omega and divergence in idempotent semirings
• Complete systems of \(\mathcal B\)-rational identities
• Group axioms for iteration
• A completeness theorem for Kleene algebras and the algebra of regular events
• Isabelle/HOL. A proof assistant for higher-order logic
• A formalisation of the Myhill-Nerode theorem based on regular expressions
• Unified Decision Procedures for Regular Expression Equivalence
• Left-Handed Completeness
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Formalising foundations of mathematics
• Automatic Proof and Disproof in Isabelle/HOL
• Une remarque sur les systèmes complets d'identités rationnelles
• Equational axioms for regular sets
• Une condition impliquant toutes les identités rationnelles
• The New Quickcheck for Isabelle
• Two Complete Axiom Systems for the Algebra of Regular Events
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
• An Efficient Coq Tactic for Deciding Kleene Algebras