equal
deleted
inserted
replaced
20 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
20 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
21 \renewcommand{\isasymequiv}{$\dn$} |
21 \renewcommand{\isasymequiv}{$\dn$} |
22 \renewcommand{\isasymemptyset}{$\varnothing$} |
22 \renewcommand{\isasymemptyset}{$\varnothing$} |
23 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
23 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
24 |
24 |
|
25 |
25 \begin{document} |
26 \begin{document} |
26 |
27 |
27 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular |
28 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular |
28 Expressions (Proof Pearl)} |
29 Expressions (Proof Pearl)} |
29 \author{Chunhan Wu\inst{1} \and Xingjuan Zhang\inst{1} \and Christian Urban\inst{2}} |
30 \author{Chunhan Wu\inst{1} \and Xingjuan Zhang\inst{1} \and Christian Urban\inst{2}} |
43 free. We show in this paper that a central result from formal |
44 free. We show in this paper that a central result from formal |
44 language theory---the Myhill-Nerode theorem---can be recreated |
45 language theory---the Myhill-Nerode theorem---can be recreated |
45 using only regular expressions. |
46 using only regular expressions. |
46 \end{abstract} |
47 \end{abstract} |
47 |
48 |
|
49 |
48 \input{session} |
50 \input{session} |
49 |
51 |
50 \bibliographystyle{plain} |
52 \bibliographystyle{plain} |
51 \bibliography{root} |
53 \bibliography{root} |
52 |
54 |