--- a/Journal/document/root.tex Fri Apr 20 11:27:49 2012 +0000
+++ b/Journal/document/root.tex Fri Apr 20 11:45:06 2012 +0000
@@ -1,4 +1,4 @@
-\documentclass{ita}
+\documentclass[acmtocl]{acmtrans2m}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
@@ -9,13 +9,12 @@
\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
\usetikzlibrary{matrix}
-\usepackage{pdfsetup}
+%%\usepackage{pdfsetup}
\usepackage{ot1patch}
\usepackage{times}
-%%\usepackage{proof}
-%%\usepackage{mathabx}
\usepackage{stmaryrd}
\usepackage{mathpartir}
+\usepackage{longtable}
\urlstyle{rm}
\isabellestyle{it}
@@ -35,39 +34,52 @@
\newcommand{\isasymbigplus}{\ensuremath{\bigplus}}
\newcommand{\bigplus}{\mbox{\Large\bf$+$}}
-\begin{document}
+
+\newtheorem{thrm}{Theorem}[section]
+\newtheorem{lmm}{Lemma}[section]
+\newtheorem{dfntn}{Definition}[section]
+\newtheorem{prpstn}{Proposition}[section]
+
\title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
- Expressions}
-\thanks{This is a revised and expanded version of \cite{WuZhangUrban11}.}
-\author{Chunhan Wu}\address{PLA University of Science and Technology, China}
-\author{Xingyuan Zhang}\sameaddress{1}
-\author{Christian Urban}\address{King's College London, United Kingdom}\secondaddress{corresponding author}
-\subjclass{68Q45}
-\keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover}
+ Expressions$^\star$}
+%%\thanks{This is a revised and expanded version of \cite{WuZhangUrban11}.}
+\author{Chunhan Wu\\PLA University of Science and Technology Nanjing, China \and
+Xingyuan Zhang\\PLA University of Science and Technology Nanjing, China \and
+Christian Urban\\ King's College London, United Kingdom}
\begin{abstract}
There are numerous textbooks on regular languages. Nearly all of them
-introduce the subject by describing finite automata and only mentioning on the
-side a connection with regular expressions. Unfortunately, automata are difficult
-to formalise in HOL-based theorem provers. The reason is that
-they need to be represented as graphs, matrices or functions, none of which
-are inductive datatypes. Also convenient operations for disjoint unions of
-graphs, matrices and functions are not easily formalisiable in HOL. In contrast, regular
-expressions can be defined conveniently as a datatype and a corresponding
-reasoning infrastructure comes for free. 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.
+introduce the subject by describing finite automata and only
+mentioning on the side a connection with regular
+expressions. Unfortunately, automata are not so straightforward to
+formalise in theorem provers. The reason is that a natural
+representation for automata are graphs, matrices or functions, none of
+which are inductive datatypes. Also convenient operations for disjoint
+unions of graphs, matrices and functions are not easily formalisiable
+in Isabelle/HOL, the theorem prover we are using. In contrast, regular
+expressions can be defined conveniently as a datatype and a
+corresponding reasoning infrastructure comes for free. 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.
\end{abstract}
+\category{F.4.1}{Mathematical Logic and Formal Languages}{Mechanical Theorem Proving}
+\category{F.4.3}{Mathematical Logic and Formal Languages}{Formal Languages}
+\terms{Interactive theorem proving, regular languages}
+\keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover}
+\begin{document}
+\begin{bottomstuff}
+Corresponding Author: Christian Urban, Department of Informatics, King's College London,
+Strand, London WC2R 2LS, UK. Email: christian.urban@kcl.ac.uk.\\
+$^\star$This is a revised and expanded version of \cite{WuZhangUrban11}.
+\end{bottomstuff}
\maketitle
+
\input{session}
-%%\mbox{}\\[-10mm]
-\bibliographystyle{plain}
-\bibliography{root}
-
\end{document}
%%% Local Variables: