document/root.tex
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Thu, 10 Jan 2013 01:46:51 +0000
changeset 18 a961c2e4dcea
parent 16 a959398693b5
child 19 7971da47e8c4
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
     1
\documentclass[10pt, conference, compsocconf]{IEEEtran}
8
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
     2
\usepackage{isabelle}
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
     3
\usepackage{isabellesym}
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
     4
\usepackage{times}
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
     5
\usepackage{amssymb}
1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
     6
\usepackage{mathpartir}
0
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
\usepackage{pdfsetup}
18
a961c2e4dcea updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
     8
\usepackage{tikz}
a961c2e4dcea updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
     9
\usepackage{pgf}
0
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    10
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    11
% urls in roman style, theory text in math-similar italics
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    12
\urlstyle{rm}
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
\isabellestyle{it}
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    14
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    15
% for uniform font size
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    16
%\renewcommand{\isastyle}{\isastyleminor}
1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    17
18
a961c2e4dcea updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    18
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
a961c2e4dcea updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    19
\renewcommand{\isasymequiv}{$\dn$}
a961c2e4dcea updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    20
\renewcommand{\isasymemptyset}{$\varnothing$}
a961c2e4dcea updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    21
\renewcommand{\isacharunderscore}{\mbox{$\_$}}
0
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    22
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    23
\begin{document}
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    24
16
a959398693b5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 15
diff changeset
    25
\title{Formalising Computability Theory in Isabelle/HOL}
1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    26
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    27
2
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 1
diff changeset
    28
\author{
15
90bc8cccc218 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 8
diff changeset
    29
\IEEEauthorblockN{Jian Xu, Xingyuan Zhang}
2
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 1
diff changeset
    30
\IEEEauthorblockA{PLA University of Science and Technology Nanjing, China}
1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    31
\and
2
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 1
diff changeset
    32
\IEEEauthorblockN{Christian Urban}
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 1
diff changeset
    33
\IEEEauthorblockA{King's College London, UK}
1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    34
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    35
0
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    36
\maketitle
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    37
1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    38
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    39
\begin{abstract}
16
a959398693b5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 15
diff changeset
    40
We present a formalised theory of computability in the 
a959398693b5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 15
diff changeset
    41
theorem prover Isabelle/HOL. This theorem prover is based on classical 
a959398693b5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 15
diff changeset
    42
logic which precludes \emph{direct} reasoning about computability: every 
a959398693b5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 15
diff changeset
    43
boolean predicate is either true or false because of the law of excluded 
a959398693b5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 15
diff changeset
    44
middle. The only way to reason about computability in a classical theorem 
a959398693b5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 15
diff changeset
    45
prover is to formalise a concrete model for computation. 
a959398693b5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 15
diff changeset
    46
We formalise Turing machines and relate them to abacus machines and recursive
a959398693b5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 15
diff changeset
    47
functions. Our theory can be used to formalise other computability results:
a959398693b5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 15
diff changeset
    48
we give one example about the undecidability of Wang tilings, whose proof uses
a959398693b5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 15
diff changeset
    49
the notion of a universal Turing machine.
1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    50
\end{abstract}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    51
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    52
\begin{IEEEkeywords}
16
a959398693b5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 15
diff changeset
    53
Turing Machines, Computability, Isabelle/HOL, Wang tilings
1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    54
\end{IEEEkeywords}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    55
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    56
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    57
\IEEEpeerreviewmaketitle
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    58
0
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    59
% generated text of all theories
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    60
\input{session}
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    61
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    62
% optional bibliography
7
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 2
diff changeset
    63
\bibliographystyle{abbrv}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 2
diff changeset
    64
\bibliography{root}
0
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    65
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    66
\end{document}
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    67
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    68
%%% Local Variables:
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    69
%%% mode: latex
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    70
%%% TeX-master: t
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    71
%%% End: