\documentclass[runningheads]{llncs}+ −
%\documentclass[10pt, conference, compsocconf]{IEEEtran}+ −
\usepackage{isabelle}+ −
\usepackage{isabellesym}+ −
\usepackage{times}+ −
\usepackage{amssymb}+ −
\usepackage{amsmath}+ −
\usepackage{mathpartir}+ −
\usepackage{pdfsetup}+ −
\usepackage{tikz}+ −
\usepackage{pgf}+ −
+ −
%% for testing+ −
\usepackage{endnotes}+ −
\let\footnote=\endnote+ −
+ −
% urls in roman style, theory text in math-similar italics+ −
\urlstyle{rm}+ −
\isabellestyle{it}+ −
+ −
% for uniform font size+ −
%\renewcommand{\isastyle}{\isastyleminor}+ −
+ −
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}+ −
\renewcommand{\isasymequiv}{$\dn$}+ −
\renewcommand{\isasymemptyset}{$\varnothing$}+ −
\renewcommand{\isacharunderscore}{\mbox{$\_$}}+ −
\renewcommand{\isasymiota}{}+ −
\newcommand{\isasymulcorner}{$\ulcorner$}+ −
\newcommand{\isasymurcorner}{$\urcorner$}+ −
\begin{document}+ −
+ −
+ −
\title{Mechanising Computability Theory in Isabelle/HOL}+ −
\author{Jian Xu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}+ −
\institute{PLA University of Science and Technology, China \and King's College London, UK}+ −
+ −
\maketitle+ −
+ −
+ −
\begin{abstract}+ −
We present a formalised theory of computability in the + −
theorem prover Isabelle/HOL. This theorem prover is based on classical + −
logic which precludes \emph{direct} reasoning about computability: every + −
boolean predicate is either true or false because of the law of excluded + −
middle. The only way to reason about computability in a classical theorem + −
prover is to formalise a concrete model for computation. + −
We formalise Turing machines and relate them to abacus machines and recursive+ −
functions. Our theory can be used to formalise other computability results:+ −
{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses+ −
the notion of a universal Turing machine.}+ −
\end{abstract}+ −
+ −
% generated text of all theories+ −
\input{session}+ −
+ −
% optional bibliography+ −
\bibliographystyle{abbrv}+ −
\bibliography{root}+ −
+ −
\end{document}+ −
+ −
%%% Local Variables:+ −
%%% mode: latex+ −
%%% TeX-master: t+ −
%%% End:+ −