1 \documentclass[acmtocl,final]{acmtrans2m} |
1 \documentclass[final, natbib]{svjour3} |
|
2 %\documentclass[acmtocl,final]{acmtrans2m} |
2 \usepackage{isabelle} |
3 \usepackage{isabelle} |
3 \usepackage{isabellesym} |
4 \usepackage{isabellesym} |
4 \usepackage{amsmath} |
5 \usepackage{amsmath} |
5 \usepackage{amssymb} |
6 \usepackage{amssymb} |
6 \usepackage{tikz} |
7 \usepackage{tikz} |
7 \usepackage{pgf} |
8 \usepackage{pgf} |
8 \usetikzlibrary{arrows,automata,decorations,fit,calc} |
9 \usetikzlibrary{arrows,automata,decorations,fit,calc} |
9 \usetikzlibrary{shapes,shapes.arrows,snakes,positioning} |
10 \usetikzlibrary{shapes,shapes.arrows,snakes,positioning} |
10 \usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf |
11 \usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf |
11 \usetikzlibrary{matrix} |
12 \usetikzlibrary{matrix} |
12 %%%\usepackage{pdfsetup} |
13 \usepackage{pdfsetup} |
13 \usepackage{ot1patch} |
14 \usepackage{ot1patch} |
14 \usepackage{times} |
15 \usepackage{times} |
15 \usepackage{stmaryrd} |
16 \usepackage{stmaryrd} |
16 \usepackage{mathpartir} |
17 \usepackage{mathpartir} |
17 \usepackage{longtable} |
18 \usepackage{longtable} |
|
19 %%\usepackage{chicago} |
|
20 |
|
21 \def\citeN{\citet} |
|
22 |
|
23 %%\journalname{Journal of Automated Reasoning} |
18 |
24 |
19 \urlstyle{rm} |
25 \urlstyle{rm} |
20 \isabellestyle{it} |
26 \isabellestyle{it} |
21 \renewcommand{\isastyleminor}{\it}% |
27 \renewcommand{\isastyleminor}{\it}% |
22 \renewcommand{\isastyle}{\normalsize\it}% |
28 \renewcommand{\isastyle}{\normalsize\it}% |
38 \newtheorem{thrm}{Theorem}[section] |
44 \newtheorem{thrm}{Theorem}[section] |
39 \newtheorem{lmm}{Lemma}[section] |
45 \newtheorem{lmm}{Lemma}[section] |
40 \newtheorem{dfntn}{Definition}[section] |
46 \newtheorem{dfntn}{Definition}[section] |
41 \newtheorem{prpstn}{Proposition}[section] |
47 \newtheorem{prpstn}{Proposition}[section] |
42 |
48 |
|
49 \begin{document} |
43 |
50 |
44 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular |
51 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular |
45 Expressions$^\star$} |
52 Expressions$^\star$\thanks{$^\star$ This is a revised and much expanded version of \cite{WuZhangUrban11}.}} |
46 %%\thanks{This is a revised and expanded version of \cite{WuZhangUrban11}.} |
53 %\author{Chunhan Wu\\PLA University of Science and Technology Nanjing, China \and |
47 \author{Chunhan Wu\\PLA University of Science and Technology Nanjing, China \and |
54 %Xingyuan Zhang\\PLA University of Science and Technology Nanjing, China \and |
48 Xingyuan Zhang\\PLA University of Science and Technology Nanjing, China \and |
55 %Christian Urban\\ King's College London, United Kingdom} |
49 Christian Urban\\ King's College London, United Kingdom} |
|
50 |
56 |
51 \markboth{C.~Wu et al.}{A Formalisation of the Myhill-Nerode Theorem based on Regular |
57 \author{Chunhan Wu \and Xingyuan Zhang \and Christian Urban} |
52 Expressions} |
58 \institute{Chunhan Wu \and Xingyuan Zhang \at PLA University of Science and Technology Nanjing, China \and |
|
59 Christian Urban \at King's College London, United Kingdom} |
|
60 |
|
61 \date{Received: date / Accepted: date} |
|
62 |
|
63 %\markboth{C.~Wu et al.}{A Formalisation of the Myhill-Nerode Theorem based on Regular |
|
64 % Expressions} |
|
65 \maketitle |
|
66 |
53 |
67 |
54 \begin{abstract} |
68 \begin{abstract} |
55 There are numerous textbooks on regular languages. Many of them focus |
69 There are numerous textbooks on regular languages. Many of them focus |
56 on finite automata for proving properties. Unfortunately, automata |
70 on finite automata for proving properties. Unfortunately, automata |
57 are not so straightforward to formalise in theorem provers. The reason |
71 are not so straightforward to formalise in theorem provers. The reason |
62 provers. We show in this paper that a central result from formal |
76 provers. We show in this paper that a central result from formal |
63 language theory---the Myhill-Nerode Theorem---can be recreated using |
77 language theory---the Myhill-Nerode Theorem---can be recreated using |
64 only regular expressions. From this theorem many closure properties of |
78 only regular expressions. From this theorem many closure properties of |
65 regular languages follow. |
79 regular languages follow. |
66 \end{abstract} |
80 \end{abstract} |
67 \category{F.4.1}{Mathematical Logic and Formal Languages}{Mechanical Theorem Proving} |
81 %\category{F.4.1}{Mathematical Logic and Formal Languages}{Mechanical Theorem Proving} |
68 \category{F.4.3}{Mathematical Logic and Formal Languages}{Formal Languages} |
82 %\category{F.4.3}{Mathematical Logic and Formal Languages}{Formal Languages} |
69 \terms{Interactive theorem proving, regular languages} |
83 %\terms{Interactive theorem proving, regular languages} |
70 \keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover} |
84 %\keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover} |
71 \begin{document} |
85 %\begin{document} |
72 \begin{bottomstuff} |
86 |
73 Corresponding Author: Christian Urban, Department of Informatics, King's College London, |
87 %\begin{bottomstuff} |
74 Strand, London WC2R 2LS, UK. Email: christian.urban@kcl.ac.uk.\\ |
88 %Corresponding Author: Christian Urban, Department of Informatics, King's College London, |
75 $^\star$This is a revised and expanded version of \cite{WuZhangUrban11}. |
89 %Strand, London WC2R 2LS, UK. Email: christian.urban@kcl.ac.uk.\\ |
76 \end{bottomstuff} |
90 %$^\star$This is a revised and expanded version of \cite{WuZhangUrban11}. |
77 \maketitle |
91 %\end{bottomstuff} |
|
92 %%\maketitle |
78 |
93 |
79 |
94 |
80 \input{session} |
95 \input{session} |
81 |
96 |
82 \end{document} |
97 \end{document} |