equal
deleted
inserted
replaced
1 \documentclass[runningheads]{llncs} |
1 \documentclass{ita} |
2 \usepackage{isabelle} |
2 \usepackage{isabelle} |
3 \usepackage{isabellesym} |
3 \usepackage{isabellesym} |
4 \usepackage{amsmath} |
4 \usepackage{amsmath} |
5 \usepackage{amssymb} |
5 \usepackage{amssymb} |
6 \usepackage{tikz} |
6 \usepackage{tikz} |
13 \usepackage{ot1patch} |
13 \usepackage{ot1patch} |
14 \usepackage{times} |
14 \usepackage{times} |
15 %%\usepackage{proof} |
15 %%\usepackage{proof} |
16 %%\usepackage{mathabx} |
16 %%\usepackage{mathabx} |
17 \usepackage{stmaryrd} |
17 \usepackage{stmaryrd} |
18 |
|
19 \titlerunning{Myhill-Nerode using Regular Expressions} |
|
20 |
18 |
21 |
19 |
22 \urlstyle{rm} |
20 \urlstyle{rm} |
23 \isabellestyle{it} |
21 \isabellestyle{it} |
24 \renewcommand{\isastyleminor}{\it}% |
22 \renewcommand{\isastyleminor}{\it}% |
34 \newcommand{\isasymbigplus}{\ensuremath{\bigplus}} |
32 \newcommand{\isasymbigplus}{\ensuremath{\bigplus}} |
35 |
33 |
36 \newcommand{\bigplus}{\mbox{\Large\bf$+$}} |
34 \newcommand{\bigplus}{\mbox{\Large\bf$+$}} |
37 \begin{document} |
35 \begin{document} |
38 |
36 |
39 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular |
37 \title{A Formalisation of the Myhill-Nerode Theorem based on Regular |
40 Expressions (Proof Pearl)} |
38 Expressions} |
41 \author{Chunhan Wu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}} |
39 \author{Chunhan Wu}\address{PLA University of Science and Technology, China} |
42 \institute{PLA University of Science and Technology, China \and TU Munich, Germany} |
40 \author{Xingyuan Zhang}\sameaddress{1} |
43 \maketitle |
41 \author{Christian Urban}\address{TU Munich, |
|
42 Germany}\secondaddress{corresponding author} |
44 |
43 |
45 %\mbox{}\\[-10mm] |
|
46 \begin{abstract} |
44 \begin{abstract} |
47 There are numerous textbooks on regular languages. Nearly all of them |
45 There are numerous textbooks on regular languages. Nearly all of them |
48 introduce the subject by describing finite automata and only mentioning on the |
46 introduce the subject by describing finite automata and only mentioning on the |
49 side a connection with regular expressions. Unfortunately, automata are difficult |
47 side a connection with regular expressions. Unfortunately, automata are difficult |
50 to formalise in HOL-based theorem provers. The reason is that |
48 to formalise in HOL-based theorem provers. The reason is that |
53 graphs and functions are not easily formalisiable in HOL. In contrast, regular |
51 graphs and functions are not easily formalisiable in HOL. In contrast, regular |
54 expressions can be defined conveniently as a datatype and a corresponding |
52 expressions can be defined conveniently as a datatype and a corresponding |
55 reasoning infrastructure comes for free. We show in this paper that a central |
53 reasoning infrastructure comes for free. We show in this paper that a central |
56 result from formal language theory---the Myhill-Nerode theorem---can be |
54 result from formal language theory---the Myhill-Nerode theorem---can be |
57 recreated using only regular expressions. |
55 recreated using only regular expressions. |
58 |
|
59 \end{abstract} |
56 \end{abstract} |
60 |
57 \maketitle |
61 |
58 |
62 \input{session} |
59 \input{session} |
63 |
60 |
64 %%\mbox{}\\[-10mm] |
61 %%\mbox{}\\[-10mm] |
65 \bibliographystyle{plain} |
62 \bibliographystyle{plain} |