A Compact Proof of Decidability for Regular Expression Equivalence

DOI10.1007/978-3-642-32347-8_19MaRDI QIDQ2914749zbMATH OpenOpenAlexFDO

Authors Andrea Asperti

Publication date 20 September 2012

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

Full work available at URL https://doi.org/10.1007/978-3-642-32347-8_19

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Recommendations

• A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions
• A Decision Procedure for Regular Expression Equivalence in Type Theory
• Deciding definability by deterministic regular expressions
• Deciding definability by deterministic regular expressions
• Extended regular expressions: succinctness and decidability
• Extended Regular Expressions: Succinctness and Decidability
• Unified decision procedures for regular expression equivalence
• scientific article; zbMATH DE number 871236
• A Finite Axiomatization of Nondeterministic Regular Expressions
• scientific article; zbMATH DE number 7774242

Cited in

(20)

• Deciding Kleene algebra terms equivalence in Coq
• A formalisation of the Myhill-Nerode theorem based on regular expressions
• Proof Pearl: regular expression equivalence and relation algebra
• On regular expression proof complexity
• Unified decision procedures for regular expression equivalence
• Deciding regular expressions (in-)equivalence in Coq
• A Decision Procedure for Bisimilarity of Generalized Regular Expressions
• A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
• A Decision Procedure for Regular Expression Equivalence in Type Theory
• Extended Regular Expressions: Succinctness and Decidability
• Proof of Correctness of a Direct Construction of DFA from Regular Expression
• scientific article; zbMATH DE number 871236 (Why is no real title available?)
• scientific article; zbMATH DE number 1416105 (Why is no real title available?)
• scientific article; zbMATH DE number 7315073 (Why is no real title available?)
• Testing the equivalence of regular languages
• Verified decision procedures for MSO on words based on derivatives of regular expressions
• Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification
• Relations between equation automata and follow automata
• A sound and complete projection for global types
• An SMT solver for regular expressions and linear arithmetic over string length

Describes a project that uses

Uses Software

• Matita
• Coq/SSReflect

This page was built for publication: A Compact Proof of Decidability for Regular Expression Equivalence

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2914749)