An Efficient Coq Tactic for Deciding Kleene Algebras
From MaRDI portal
Publication:5747648
DOI10.1007/978-3-642-14052-5_13zbMath1291.68330OpenAlexW1600140070MaRDI QIDQ5747648
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
Related Items
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
This page was built for publication: An Efficient Coq Tactic for Deciding Kleene Algebras
