35 \newcommand{\isasymulcorner}{$\ulcorner$} |
35 \newcommand{\isasymulcorner}{$\ulcorner$} |
36 \newcommand{\isasymurcorner}{$\urcorner$} |
36 \newcommand{\isasymurcorner}{$\urcorner$} |
37 \begin{document} |
37 \begin{document} |
38 |
38 |
39 |
39 |
40 \title{Mechanising Computability Theory in Isabelle/HOL} |
40 \title{Mechanising Turing Machines and Computability Theory in Isabelle/HOL} |
41 \author{Jian Xu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}} |
41 \author{Jian Xu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}} |
42 \institute{PLA University of Science and Technology, China \and King's College London, UK} |
42 \institute{PLA University of Science and Technology, China \and King's College London, UK} |
43 |
43 |
44 \maketitle |
44 \maketitle |
45 |
45 |
46 |
46 |
47 \begin{abstract} |
47 \begin{abstract} |
48 We present a formalised theory of computability in the |
48 We present a formalised theory of computability in the theorem prover |
49 theorem prover Isabelle/HOL. This theorem prover is based on classical |
49 Isabelle/HOL. This theorem prover is based on classical logic which |
50 logic which precludes \emph{direct} reasoning about computability: every |
50 precludes \emph{direct} reasoning about computability: every boolean |
51 boolean predicate is either true or false because of the law of excluded |
51 predicate is either true or false because of the law of excluded |
52 middle. The only way to reason about computability in a classical theorem |
52 middle. The only way to reason about computability in a classical |
53 prover is to formalise a concrete model for computation. |
53 theorem prover is to formalise a concrete model for computation. We |
54 We formalise Turing machines and relate them to abacus machines and recursive |
54 formalise Turing machines and relate them to abacus machines and |
55 functions. Our theory can be used to formalise other computability results: |
55 recursive functions. We also formalise a universal Turing machine and |
56 {\it we give one example about the undecidability of Wang's tiling problem, whose proof uses |
56 reasoning techniques that allow us to reason about Turing machine |
57 the notion of a universal Turing machine.} |
57 programs. Our theory can be used to formalise other computability |
|
58 results. We give one example about the computational equivalence of |
|
59 single-sided Turing machines. |
|
60 %{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses |
|
61 %the notion of a universal Turing machine.} |
58 \end{abstract} |
62 \end{abstract} |
59 |
63 |
60 % generated text of all theories |
64 % generated text of all theories |
61 \input{session} |
65 \input{session} |
62 |
66 |