A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)

DOI10.1007/978-3-642-22863-6_25MaRDI QIDQ3088018zbMATH OpenOpenAlexFDO

Authors Chunhan Wu, Christian Urban, Xingyuan Zhang

Publication date 17 August 2011

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

Full work available at URL https://doi.org/10.1007/978-3-642-22863-6_25

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Recommendations

• A formalisation of the Myhill-Nerode theorem based on regular expressions
• A constructive theory of regular languages in Coq
• A Compact Proof of Decidability for Regular Expression Equivalence
• Automated analysis of regular algebra
• On the fine-structure of regular algebra

Cites work

• scientific article; zbMATH DE number 1033559 (Why is no real title available?)
• scientific article; zbMATH DE number 2085164 (Why is no real title available?)
• scientific article; zbMATH DE number 3311755 (Why is no real title available?)
• Adapting functional programs to higher order logic
• Derivatives of Regular Expressions
• Formalizing the Logic-Automaton Connection
• Regular-expression derivatives re-examined

Cited in

(12)

• A Decision Procedure for Regular Expression Equivalence in Type Theory
• A formalisation of the Myhill-Nerode theorem based on regular expressions
• A Mechanized Proof of Higman’s Lemma by Open Induction
• Certified Kruskal's tree theorem
• A Verified Compositional Algorithm for AI Planning
• Formally verified algorithms for upper-bounding state space diameters
• Regular language representations in the constructive type theory of Coq
• Proof Pearl: regular expression equivalence and relation algebra
• Automated analysis of regular algebra
• Pumping, with or without choice
• Automated Reasoning in Higher-Order Regular Algebra
• A formalisation of finite automata using hereditarily finite sets

Describes a project that uses

Uses Software

• Presburger Automata
• Myhill-Nerode

This page was built for publication: A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)

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