equal
deleted
inserted
replaced
20 \urlstyle{rm} |
20 \urlstyle{rm} |
21 \isabellestyle{it} |
21 \isabellestyle{it} |
22 \renewcommand{\isastyleminor}{\it}% |
22 \renewcommand{\isastyleminor}{\it}% |
23 \renewcommand{\isastyle}{\normalsize\it}% |
23 \renewcommand{\isastyle}{\normalsize\it}% |
24 |
24 |
|
25 \newcommand*{\threesim}{% |
|
26 \mathrel{\vcenter{\offinterlineskip |
|
27 \hbox{$\sim$}\vskip-.35ex\hbox{$\sim$}\vskip-.35ex\hbox{$\sim$}}}} |
25 |
28 |
26 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
29 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
27 \renewcommand{\isasymequiv}{$\dn$} |
30 \renewcommand{\isasymequiv}{$\dn$} |
28 \renewcommand{\isasymemptyset}{$\varnothing$} |
31 \renewcommand{\isasymemptyset}{$\varnothing$} |
29 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
32 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
34 \newcommand{\bigplus}{\mbox{\Large\bf$+$}} |
37 \newcommand{\bigplus}{\mbox{\Large\bf$+$}} |
35 \begin{document} |
38 \begin{document} |
36 |
39 |
37 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular |
40 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular |
38 Expressions} |
41 Expressions} |
|
42 \thanks{This is a revised and expanded version of ???} |
39 \author{Chunhan Wu}\address{PLA University of Science and Technology, China} |
43 \author{Chunhan Wu}\address{PLA University of Science and Technology, China} |
40 \author{Xingyuan Zhang}\sameaddress{1} |
44 \author{Xingyuan Zhang}\sameaddress{1} |
41 \author{Christian Urban}\address{TU Munich, |
45 \author{Christian Urban}\address{TU Munich, |
42 Germany}\secondaddress{corresponding author} |
46 Germany}\secondaddress{corresponding author} |
|
47 \subjclass{68Q45} |
|
48 \keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover} |
43 |
49 |
44 \begin{abstract} |
50 \begin{abstract} |
45 There are numerous textbooks on regular languages. Nearly all of them |
51 There are numerous textbooks on regular languages. Nearly all of them |
46 introduce the subject by describing finite automata and only mentioning on the |
52 introduce the subject by describing finite automata and only mentioning on the |
47 side a connection with regular expressions. Unfortunately, automata are difficult |
53 side a connection with regular expressions. Unfortunately, automata are difficult |