equal
deleted
inserted
replaced
37 \newcommand{\bigplus}{\mbox{\Large\bf$+$}} |
37 \newcommand{\bigplus}{\mbox{\Large\bf$+$}} |
38 \begin{document} |
38 \begin{document} |
39 |
39 |
40 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular |
40 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular |
41 Expressions} |
41 Expressions} |
42 \thanks{This is a revised and expanded version of ???} |
42 \thanks{This is a revised and expanded version of \cite{WuZhangUrban11}.} |
43 \author{Chunhan Wu}\address{PLA University of Science and Technology, China} |
43 \author{Chunhan Wu}\address{PLA University of Science and Technology, China} |
44 \author{Xingyuan Zhang}\sameaddress{1} |
44 \author{Xingyuan Zhang}\sameaddress{1} |
45 \author{Christian Urban}\address{TU Munich, |
45 \author{Christian Urban}\address{TU Munich, |
46 Germany}\secondaddress{corresponding author} |
46 Germany}%%\secondaddress{corresponding author} |
47 \subjclass{68Q45} |
47 \subjclass{68Q45} |
48 \keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover} |
48 \keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover} |
49 |
49 |
50 \begin{abstract} |
50 \begin{abstract} |
51 There are numerous textbooks on regular languages. Nearly all of them |
51 There are numerous textbooks on regular languages. Nearly all of them |