equal
deleted
inserted
replaced
52 We present a formalised theory of computability in the theorem prover |
52 We present a formalised theory of computability in the theorem prover |
53 Isabelle/HOL. This theorem prover is based on classical logic which |
53 Isabelle/HOL. This theorem prover is based on classical logic which |
54 precludes \emph{direct} reasoning about computability: every boolean |
54 precludes \emph{direct} reasoning about computability: every boolean |
55 predicate is either true or false because of the law of excluded |
55 predicate is either true or false because of the law of excluded |
56 middle. The only way to reason about computability in a classical |
56 middle. The only way to reason about computability in a classical |
57 theorem prover is to formalise a concrete model for computation. We |
57 theorem prover is to formalise a concrete model of computation. We |
58 formalise Turing machines and relate them to abacus machines and |
58 formalise Turing machines and relate them to abacus machines and |
59 recursive functions. We also formalise a universal Turing machine and |
59 recursive functions. We also formalise a universal Turing machine and |
60 Hoare-style reasoning techniques that allow us to reason about Turing machine |
60 Hoare-style reasoning techniques that allow us to reason about Turing machine |
61 programs. Our theory can be used to formalise other computability |
61 programs. Our theory can be used to formalise other computability |
62 results. We give one example about the computational equivalence of |
62 results. We give one example about the computational equivalence of |