1 \documentclass{llncs}

     2 \usepackage{isabelle}

     3 \usepackage{isabellesym}

     4 \usepackage{amsmath}

     5 \usepackage{amssymb}

     6 \usepackage{tikz}

     7 \usepackage{pgf}

     8 \usepackage{pdfsetup}

     9 \usepackage{ot1patch}

    10 \usepackage{times}

    11 \usepackage{proof}

    12 

    13 

    14 \urlstyle{rm}

    15 \isabellestyle{it}

    16 \renewcommand{\isastyleminor}{\it}%

    17 \renewcommand{\isastyle}{\normalsize\it}%

    18 

    19 

    20 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}

    21 \renewcommand{\isasymequiv}{$\dn$}

    22 \renewcommand{\isasymemptyset}{$\varnothing$}

    23 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}

    24 

    25 \begin{document}

    26 

    27 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular Expressions}

    28 \author{Chunhan Wu\inst{1} \and Xingjuan Zhang\inst{1} \and Christian Urban\inst{2}}

    29 \institute{PLA University, China \and TU Munich, Germany}

    30 \maketitle

    31 

    32 \begin{abstract} 

    33 There are numerous textbooks on regular languages. Nearly all of them 

    34 introduce the subject by describing finite automata and 

    35 only mentioning on the side a connection with regular expressions. 

    36 Unfortunately, automata are a hassle for formalisations in HOL-based

    37 theorem provers. The reason is they need to be represented as graphs 

    38 or matrices, neither of which can be easily defined as datatype. Also 

    39 operations, such as disjoint union of graphs, are not easily formalisiable 

    40 in HOL. In contrast, regular expressions can be defined easily 

    41 as datatype and a corresponding reasoning infrastructure comes for 

    42 free. We show in this paper that a central result from formal 

    43 language theory---the Myhill-Nerode theorem---can be recreated 

    44 using only regular expressions. 

    45 \end{abstract}

    46 

    47 \input{session}

    48 

    49 \bibliographystyle{plain}

    50 \bibliography{root}

    51 

    52 \end{document}

    53 

    54 %%% Local Variables:

    55 %%% mode: latex

    56 %%% TeX-master: t

    57 %%% End: