tm: document/root.tex@a959398693b5 (annotated)

1 4b9aa15ff713 added 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 4b9aa15ff713 added 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}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9	% 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	10	\urlstyle{rm}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11	\isabellestyle{it}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	13	% for uniform font size
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	%\renewcommand{\isastyle}{\isastyleminor}
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	15
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	\begin{document}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18
16 a959398693b5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 15 diff changeset	19	\title{Formalising Computability Theory in Isabelle/HOL}
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	20
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	21
2 26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	22	\author{
15 90bc8cccc218 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 8 diff changeset	23	\IEEEauthorblockN{Jian Xu, Xingyuan Zhang}
2 26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	24	\IEEEauthorblockA{PLA University of Science and Technology Nanjing, China}
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	25	\and
2 26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	26	\IEEEauthorblockN{Christian Urban}
26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	27	\IEEEauthorblockA{King's College London, UK}
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	28	}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	29
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30	\maketitle
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	32
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	33	\begin{abstract}
16 a959398693b5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 15 diff changeset	34	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	35	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	36	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	37	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	38	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	39	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	40	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	41	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	42	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	43	the notion of a universal Turing machine.
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	44	\end{abstract}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	45
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	46	\begin{IEEEkeywords}
16 a959398693b5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 15 diff changeset	47	Turing Machines, Computability, Isabelle/HOL, Wang tilings
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	48	\end{IEEEkeywords}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	49
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	50
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	51	\IEEEpeerreviewmaketitle
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	52
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	53	% generated text of all theories
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	54	\input{session}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	55
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	56	% optional bibliography
7 f7896d90aa19 more Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	57	\bibliographystyle{abbrv}
f7896d90aa19 more Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	58	\bibliography{root}
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	59
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	60	\end{document}
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	%%% Local Variables:
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	63	%%% mode: latex
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	64	%%% TeX-master: t
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	65	%%% End:

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Tue, 08 Jan 2013 01:21:02 +0000
changeset 16	a959398693b5
parent 15	90bc8cccc218
child 18	a961c2e4dcea
permissions	-rw-r--r--