Myhill-Nerode

MaRDI QIDQ40261swMATHFDO

Authors Chunhan Wu, Xingyuan Zhang, Christian Urban, Manuel Eberl

Publication date 26 August 2011

Official website https://www.isa-afp.org/entries/Myhill-Nerode.html

Cites work

• A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
• Partial derivatives of regular expressions and finite automaton constructions

Described by source

• A formalisation of the Myhill-Nerode theorem based on regular expressions

Cited in

(23)

• Formally verified algorithms for upper-bounding state space diameters
• Regular language representations in the constructive type theory of Coq
• On the fine-structure of regular algebra
• Two-Way Automata in Coq
• A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions
• Automated Reasoning in Higher-Order Regular Algebra
• A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
• A Decision Procedure for Regular Expression Equivalence in Type Theory
• A Mechanized Proof of Higman’s Lemma by Open Induction
• Presburger Automata
• Gauss Jordan Elimination
• Well Quasi Orders
• Regular Sets
• Hotel Key Card
• Hereditarily Finite Sets
• Finite Automata HF
• Decreasing Diagrams II
• Worker/Wrapper Transformation
• Regex_Equivalence
• MSO_Regex_Equivalence
• Open Induction
• Verified decision procedures for MSO on words based on derivatives of regular expressions
• A Verified Compositional Algorithm for AI Planning

This page was built for software: Myhill-Nerode