Myhill-Nerode
From MaRDI portal
swMATH28547MaRDI QIDQ40261FDOQ40261
Author name not available (Why is that?)
Official website: https://www.isa-afp.org/entries/Myhill-Nerode.html
Cited In (23)
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- On the fine-structure of regular algebra
- A Mechanized Proof of Higman’s Lemma by Open Induction
- 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
- A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
- Gauss Jordan Elimination
- Presburger Automata
- Regular Sets
- Finite Automata HF
- Hotel Key Card
- Hereditarily Finite Sets
- Decreasing Diagrams II
- Well Quasi Orders
- Worker/Wrapper Transformation
- MSO_Regex_Equivalence
- Regex_Equivalence
- Verified decision procedures for MSO on words based on derivatives of regular expressions
- Open Induction
- A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions
- Two-Way Automata in Coq
- Automated Reasoning in Higher-Order Regular Algebra
This page was built for software: Myhill-Nerode
