Myhill-Nerode swMATH ID: 28547 Software Authors: Wu, Chunhan; Zhang, Xingyuan; Urban, Christian Description: A formalisation of the Myhill-Nerode theorem based on regular expressions. There are numerous textbooks on regular languages. Many of them focus on finite automata for proving properties. Unfortunately, automata are not so straightforward to formalise in theorem provers. The reason is that natural representations for automata are graphs, matrices or functions, none of which are inductive datatypes. Regular expressions can be defined straightforwardly as a datatype and a corresponding reasoning infrastructure comes for free in theorem provers. We show in this paper that a central result from formal language theory – the Myhill-Nerode Theorem – can be recreated using only regular expressions. From this theorem many closure properties of regular languages follow. Homepage: https://www.isa-afp.org/entries/Myhill-Nerode.html Dependencies: Isabelle Keywords: regular languages; theorem provers; Myhill-Nerode theorem Related Software: Archive Formal Proofs; Regular Sets; Presburger Automata; Coq; Isabelle/HOL; MSO_Regex_Equivalence; Finite Automata HF; Hereditarily Finite Sets; Coq/SSReflect; Regex_Equivalence; CeTA; Nitpick; Isabelle; Sledgehammer; Open Induction; Decreasing Diagrams II; Well Quasi Orders; GitHub; Hotel Key Card; CAVA LTL Modelchecker Cited in: 11 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year A formalisation of the Myhill-Nerode theorem based on regular expressions. Zbl 1314.68179Wu, Chunhan; Zhang, Xingyuan; Urban, Christian 2014 all top 5 Cited by 17 Authors 2 Doczkal, Christian 2 Nipkow, Tobias 2 Smolka, Gert 2 Struth, Georg 2 Urban, Christian 2 Wu, Chunhan 2 Zhang, Xingyuan 1 Abdulaziz, Mohammad 1 Armstrong, Alasdair 1 Coquand, Thierry 1 Foster, Simon 1 Gretton, Charles 1 Haslbeck, Maximilian P. L. 1 Norrish, Michael 1 Siles, Vincent 1 Sternagel, Christian 1 Traytel, Dmitry Cited in 2 Serials 4 Journal of Automated Reasoning 1 Journal of Functional Programming Cited in 3 Fields 11 Computer science (68-XX) 3 Mathematical logic and foundations (03-XX) 1 Order, lattices, ordered algebraic structures (06-XX) Citations by Year