equal
deleted
inserted
replaced
47 |
47 |
48 \maketitle |
48 \maketitle |
49 |
49 |
50 |
50 |
51 \begin{abstract} |
51 \begin{abstract} |
52 We present a formalised theory of computability in the theorem prover |
52 We formalise results from computability theory in the theorem prover |
53 Isabelle/HOL. |
53 Isabelle/HOL. |
54 %This theorem prover is based on classical logic which |
54 %This theorem prover is based on classical logic which |
55 %precludes \emph{direct} reasoning about computability: every boolean |
55 %precludes \emph{direct} reasoning about computability: every boolean |
56 %predicate is either true or false because of the law of excluded |
56 %predicate is either true or false because of the law of excluded |
57 %middle. The only way to reason about computability in a classical |
57 %middle. The only way to reason about computability in a classical |