A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)

DOI10.1007/978-3-642-22863-6_25zbMath1342.68306OpenAlexW1500313939MaRDI QIDQ3088018

Christian Urban, Chunhan Wu, Xing-Yuan 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)

Related Items

Automated Reasoning in Higher-Order Regular Algebra ⋮ Formally verified algorithms for upper-bounding state space diameters ⋮ Regular language representations in the constructive type theory of Coq ⋮ Certified Kruskal’s Tree Theorem ⋮ A Mechanized Proof of Higman’s Lemma by Open Induction ⋮ A Verified Compositional Algorithm for AI Planning ⋮ A Decision Procedure for Regular Expression Equivalence in Type Theory ⋮ A formalisation of the Myhill-Nerode theorem based on regular expressions

Uses Software

• Myhill-Nerode
• Presburger Automata

Cites Work

• Adapting functional programs to higher order logic
• Formalizing the Logic-Automaton Connection
• Regular-expression derivatives re-examined
• Derivatives of Regular Expressions
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)