A formalisation of the Myhill-Nerode theorem based on regular expressions (Q2351151): Difference between revisions

@@ Property / describes a project that uses @@
+Presburger Automata
@@ Property / describes a project that uses: Presburger Automata / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Gauss Jordan Elimination
@@ Property / describes a project that uses: Gauss Jordan Elimination / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Regular Sets
@@ Property / describes a project that uses: Regular Sets / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-013-9297-2
+Normal rank
@@ Property / OpenAlex ID @@
+W2054695370
@@ Property / OpenAlex ID: W2054695370 / rank @@
+Normal rank
@@ Property / cites work @@
+Partial Derivative Automata Formalized in Coq
@@ Property / cites work: Partial Derivative Automata Formalized in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Partial derivatives of regular expressions and finite automaton constructions
+Normal rank
@@ Property / cites work @@
+A Compact Proof of Decidability for Regular Expression Equivalence
+Normal rank
@@ Property / cites work @@
+Q4736387
@@ Property / cites work: Q4736387 / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing the Logic-Automaton Connection
@@ Property / cites work: Formalizing the Logic-Automaton Connection / rank @@
+Normal rank
@@ Property / cites work @@
+Derivatives of Regular Expressions
@@ Property / cites work: Derivatives of Regular Expressions / rank @@
+Normal rank
@@ Property / cites work @@
+A Decision Procedure for Regular Expression Equivalence in Type Theory
+Normal rank
@@ Property / cites work @@
+A Constructive Theory of Regular Languages in Coq
@@ Property / cites work: A Constructive Theory of Regular Languages in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+The complexity of finding SUBSEQ\((A)\)
@@ Property / cites work: The complexity of finding SUBSEQ\((A)\) / rank @@
+Normal rank
@@ Property / cites work @@
+Regular-expression derivatives re-examined
@@ Property / cites work: Regular-expression derivatives re-examined / rank @@
+Normal rank
@@ Property / cites work @@
+Succinctness of the Complement and Intersection of Regular Expressions
+Normal rank
@@ Property / cites work @@
+EDUCATIONAL PEARL: ‘Proof-directed debugging’ revisited for a first-order version
+Normal rank
@@ Property / cites work @@
+On free monoids partially ordered by embedding
@@ Property / cites work: On free monoids partially ordered by embedding / rank @@
+Normal rank
@@ Property / cites work @@
+Proof-directed debugging
@@ Property / cites work: Proof-directed debugging / rank @@
+Normal rank
@@ Property / cites work @@
+Q5592246
@@ Property / cites work: Q5592246 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4344149
@@ Property / cites work: Q4344149 / rank @@
+Normal rank
@@ Property / cites work @@
+Proof Pearl: regular expression equivalence and relation algebra
+Normal rank
@@ Property / cites work @@
+Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
+Normal rank
@@ Property / cites work @@
+Adapting functional programs to higher order logic
+Normal rank
@@ Property / cites work @@
+Q3644388
@@ Property / cites work: Q3644388 / rank @@
+Normal rank
@@ Property / cites work @@
+A Second Course in Formal Languages and Automata Theory
+Normal rank
@@ Property / cites work @@
+Certified Kruskal’s Tree Theorem
@@ Property / cites work: Certified Kruskal’s Tree Theorem / rank @@
+Normal rank
@@ Property / cites work @@
+A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
+Normal rank