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

DOI10.1007/978-3-642-22863-6_25zbMATH Open1342.68306OpenAlexW1500313939MaRDI QIDQ3088018FDOQ3088018

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

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

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Cites Work

• Formalizing the Logic-Automaton Connection
• Title not available (Why is that?)
• Derivatives of Regular Expressions
• Title not available (Why is that?)
• Regular-expression derivatives re-examined
• Title not available (Why is that?)
• Adapting functional programs to higher order logic

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

Uses Software

• Myhill-Nerode
• Presburger Automata

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)