tm: Paper/document/root.tex@559e5c6e5113 (annotated)

42 00ae320bb804 added llncs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 34 diff changeset	1	\documentclass[runningheads]{llncs}
00ae320bb804 added llncs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 34 diff changeset	2	%\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	3	\usepackage{isabelle}
c216ae455c90 more on the paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 7 diff changeset	4	\usepackage{isabellesym}
c216ae455c90 more on the paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 7 diff changeset	5	\usepackage{times}
c216ae455c90 more on the paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 7 diff changeset	6	\usepackage{amssymb}
30 ba789a0768a2 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 27 diff changeset	7	\usepackage{amsmath}
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	8	\usepackage{mathpartir}
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9	\usepackage{pdfsetup}
18 a961c2e4dcea updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	10	\usepackage{tikz}
a961c2e4dcea updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	11	\usepackage{pgf}
0 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	% 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	14	\urlstyle{rm}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15	\isabellestyle{it}
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	% for uniform font size
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18	%\renewcommand{\isastyle}{\isastyleminor}
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	19
18 a961c2e4dcea updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	20	\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
a961c2e4dcea updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	21	\renewcommand{\isasymequiv}{$\dn$}
a961c2e4dcea updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	22	\renewcommand{\isasymemptyset}{$\varnothing$}
a961c2e4dcea updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	23	\renewcommand{\isacharunderscore}{\mbox{$\_$}}
27 a1e8b94d0b93 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 19 diff changeset	24	\renewcommand{\isasymiota}{}
34 22e5804b135c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 30 diff changeset	25	\newcommand{\isasymulcorner}{$\ulcorner$}
22e5804b135c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 30 diff changeset	26	\newcommand{\isasymurcorner}{$\urcorner$}
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27	\begin{document}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28
42 00ae320bb804 added llncs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 34 diff changeset	29
16 a959398693b5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 15 diff changeset	30	\title{Formalising Computability Theory in Isabelle/HOL}
42 00ae320bb804 added llncs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 34 diff changeset	31	\author{Jian Xu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}
00ae320bb804 added llncs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 34 diff changeset	32	\institute{PLA University of Science and Technology, China \and King's College London, UK}
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	33
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34	\maketitle
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	36
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	37	\begin{abstract}
16 a959398693b5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 15 diff changeset	38	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	39	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	40	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	41	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	42	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	43	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	44	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	45	functions. Our theory can be used to formalise other computability results:
48 559e5c6e5113 updated to ITP and updated directories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 42 diff changeset	46	{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses
559e5c6e5113 updated to ITP and updated directories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 42 diff changeset	47	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	48	\end{abstract}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	49
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50	% generated text of all theories
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	51	\input{session}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	52
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	53	% optional bibliography
7 f7896d90aa19 more Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	54	\bibliographystyle{abbrv}
f7896d90aa19 more Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	55	\bibliography{root}
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	56
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	57	\end{document}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	58
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	59	%%% Local Variables:
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	60	%%% mode: latex
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	61	%%% TeX-master: t
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	62	%%% End:

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Fri, 18 Jan 2013 11:40:01 +0000
changeset 48	559e5c6e5113
parent 42	document/root.tex@00ae320bb804
child 49	b388dceee892
permissions	-rw-r--r--