tm: document/root.tex@6d89ed67ba27 (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}
30 ba789a0768a2 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 27 diff changeset	6	\usepackage{amsmath}
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	7	\usepackage{mathpartir}
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8	\usepackage{pdfsetup}
18 a961c2e4dcea updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	9	\usepackage{tikz}
a961c2e4dcea updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	10	\usepackage{pgf}
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12	% 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	13	\urlstyle{rm}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	\isabellestyle{it}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16	% for uniform font size
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	%\renewcommand{\isastyle}{\isastyleminor}
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	18
18 a961c2e4dcea updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	19	\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
a961c2e4dcea updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	20	\renewcommand{\isasymequiv}{$\dn$}
a961c2e4dcea updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	21	\renewcommand{\isasymemptyset}{$\varnothing$}
a961c2e4dcea updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	22	\renewcommand{\isacharunderscore}{\mbox{$\_$}}
27 a1e8b94d0b93 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 19 diff changeset	23	\renewcommand{\isasymiota}{}
34 22e5804b135c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 30 diff changeset	24	\newcommand{\isasymulcorner}{$\ulcorner$}
22e5804b135c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 30 diff changeset	25	\newcommand{\isasymurcorner}{$\urcorner$}
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26	\begin{document}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27
16 a959398693b5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 15 diff changeset	28	\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	29
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	30
2 26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	31	\author{
15 90bc8cccc218 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 8 diff changeset	32	\IEEEauthorblockN{Jian Xu, Xingyuan Zhang}
2 26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	33	\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	34	\and
2 26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	35	\IEEEauthorblockN{Christian Urban}
26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	36	\IEEEauthorblockA{King's College London, UK}
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	37	}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	38
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39	\maketitle
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	40
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	41
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	42	\begin{abstract}
16 a959398693b5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 15 diff changeset	43	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	44	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	45	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	46	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	47	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	48	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	49	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	50	functions. Our theory can be used to formalise other computability results:
19 7971da47e8c4 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 18 diff changeset	51	we give one example about the undecidability of Wang's tiling problem, whose proof uses
16 a959398693b5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 15 diff changeset	52	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	53	\end{abstract}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	54
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	55	\begin{IEEEkeywords}
16 a959398693b5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 15 diff changeset	56	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	57	\end{IEEEkeywords}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	58
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	59
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	60	\IEEEpeerreviewmaketitle
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	61
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	62	% generated text of all theories
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	63	\input{session}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	64
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	65	% optional bibliography
7 f7896d90aa19 more Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	66	\bibliographystyle{abbrv}
f7896d90aa19 more Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	67	\bibliography{root}
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	68
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	69	\end{document}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	70
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	71	%%% Local Variables:
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	72	%%% mode: latex
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	73	%%% TeX-master: t
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	74	%%% End:

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Sun, 13 Jan 2013 23:59:29 +0000
changeset 41	6d89ed67ba27
parent 34	22e5804b135c
child 42	00ae320bb804
permissions	-rw-r--r--