tm: document/root.tex@26b17f2d583e (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}
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	2	\usepackage{isabelle,isabellesym}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4	%\usepackage{amssymb}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5	%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6	%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	7	%\<triangleq>, \<yen>, \<lozenge>
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	%\usepackage[greek,english]{babel}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	%option greek for \<euro>
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11	%option english (default language) for \<guillemotleft>, \<guillemotright>
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	%\usepackage[only,bigsqcap]{stmaryrd}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	%for \<Sqinter>
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	%\usepackage{eufrak}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	%\usepackage{textcomp}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20	%for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	21	%\<currency>
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	% this should be the last package used
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	24	\usepackage{mathpartir}
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25	\usepackage{pdfsetup}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27	% 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	28	\urlstyle{rm}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29	\isabellestyle{it}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31	% for uniform font size
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	32	%\renewcommand{\isastyle}{\isastyleminor}
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
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35	\begin{document}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36
2 26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	37	\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	38
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	39
2 26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	40	\author{
26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	41	\IEEEauthorblockN{Xu Jian, Xingyuan Zhang}
26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	42	\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	43	\and
2 26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	44	\IEEEauthorblockN{Christian Urban}
26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	45	\IEEEauthorblockA{King's College London, UK}
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	46	}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	47
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48	\maketitle
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	49
1 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	\begin{abstract}
2 26b17f2d583e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	52	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	53	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	54	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	55	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	56	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	57	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	58	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	59	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	60
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	61	\end{abstract}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	62
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	63	\begin{IEEEkeywords}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	64	Turing Machines, Decidability, Isabelle/HOL;
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	65	\end{IEEEkeywords}
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	66
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	67
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	68	\IEEEpeerreviewmaketitle
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	69
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	70
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	71	%\tableofcontents
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	72
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	73	% sane default for proof documents
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	74	\parindent 0pt\parskip 0.5ex
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	75
1 4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	76
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	77
4b9aa15ff713 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	78
0 aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	79	% generated text of all theories
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	80	\input{session}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	81
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	82	% optional bibliography
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	83	%\bibliographystyle{abbrv}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	84	%\bibliography{root}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	85
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	86	\end{document}
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	87
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	88	%%% Local Variables:
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	89	%%% mode: latex
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	90	%%% TeX-master: t
aa8656a8dbef initial setup Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	91	%%% End:

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Wed, 26 Dec 2012 19:03:06 +0000
changeset 2	26b17f2d583e
parent 1	4b9aa15ff713
child 7	f7896d90aa19
permissions	-rw-r--r--