An Efficient Coq Tactic for Deciding Kleene Algebras

DOI10.1007/978-3-642-14052-5_13zbMath1291.68330OpenAlexW1600140070MaRDI QIDQ5747648

Thomas Braibant, Damien Pous

Publication date: 14 September 2010

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14052-5_13

Mathematics Subject Classification ID

Algebraic theory of languages and automata (68Q70)

Related Items (18)

Trakhtenbrot’s Theorem in Coq ⋮ Automated Reasoning in Higher-Order Regular Algebra ⋮ Deciding Regular Expressions (In-)Equivalence in Coq ⋮ On Completeness of Omega-Regular Algebras ⋮ Proof Pearl: regular expression equivalence and relation algebra ⋮ Typing theorems of omega algebra ⋮ Programming and automating mathematics in the Tarski-Kleene hierarchy ⋮ Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version ⋮ On tools for completeness of Kleene algebra with hypotheses ⋮ Verified decision procedures for MSO on words based on derivatives of regular expressions ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Building program construction and verification tools from algebraic principles ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates ⋮ A Decision Procedure for Regular Expression Equivalence in Type Theory ⋮ Tactics for Reasoning Modulo AC in Coq ⋮ Deciding Kleene algebra terms equivalence in Coq ⋮ On the fine-structure of regular algebra

Uses Software

• Coq
• Isabelle/Isar
• RALL
• CoLoR
• ATBR

This page was built for publication: An Efficient Coq Tactic for Deciding Kleene Algebras