tm: document/root.tex@b92529dc95c5 (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
2 26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	19	\title{A Formalised Theory of Turing Machines 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{
26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	23	\IEEEauthorblockN{Xu Jian, Xingyuan Zhang}
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}
2 26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	34	Isabelle/HOL is an interactive theorem prover based on classical
26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	35	logic. While classical reasoning allow users to take convenient
26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	36	shortcuts in some proofs, it precludes \emph{direct} reasoning about
26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	37	decidability: every boolean predicate is either true or false
26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	38	because of the law of excluded middle. The only way to reason
26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	39	about decidability in a classical theorem prover, like Isabelle/HOL,
26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	40	is to formalise a concrete model for computation. In this paper
26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	41	we formalise Turing machines and relate them to register machines.
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	42
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	43	\end{abstract}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	44
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	45	\begin{IEEEkeywords}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	46	Turing Machines, Decidability, Isabelle/HOL;
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	47	\end{IEEEkeywords}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	48
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	\IEEEpeerreviewmaketitle
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	51
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	52	% generated text of all theories
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	53	\input{session}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	54
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	55	% optional bibliography
7 f7896d90aa19 more Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	56	\bibliographystyle{abbrv}
f7896d90aa19 more Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	57	\bibliography{root}
0 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	\end{document}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	60
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	61	%%% Local Variables:
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	62	%%% mode: latex
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	63	%%% TeX-master: t
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	64	%%% End:

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Sat, 05 Jan 2013 00:31:43 +0000
changeset 14	b92529dc95c5
parent 8	c216ae455c90
child 15	90bc8cccc218
permissions	-rw-r--r--