equal
deleted
inserted
replaced
57 theorem prover is to formalise a concrete model of 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 |
63 single-sided Turing machines. |
63 %single-sided Turing machines. |
64 %{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses |
64 %{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses |
65 %the notion of a universal Turing machine.} |
65 %the notion of a universal Turing machine.} |
66 \end{abstract} |
66 \end{abstract} |
67 |
67 |
68 % generated text of all theories |
68 % generated text of all theories |