Myhill-Nerode

swMATH28547MaRDI QIDQ40261FDOQ40261

Author name not available (Why is that?)

Described by source

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

Cited In (11)

• 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
• Verified decision procedures for MSO on words based on derivatives of regular expressions
• A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions
• Two-Way Automata in Coq
• A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
• Automated Reasoning in Higher-Order Regular Algebra

This page was built for software: Myhill-Nerode