Myhill-Nerode
From MaRDI portal
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
