On the fine-structure of regular algebra
From MaRDI portal
Publication:2352506
DOI10.1007/s10817-014-9318-9zbMath1331.68128OpenAlexW2056135689MaRDI QIDQ2352506
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
regular languagesautomated theorem provinginteractive theorem provingKleene algebraformalised mathematicsregular algebra
Related Items
Completeness and the finite model property for Kleene algebra, reconsidered, Left-handed completeness, Regular_Algebras
Uses Software
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
