equal
deleted
inserted
replaced
43 boolean predicate is either true or false because of the law of excluded |
43 boolean predicate is either true or false because of the law of excluded |
44 middle. The only way to reason about computability in a classical theorem |
44 middle. The only way to reason about computability in a classical theorem |
45 prover is to formalise a concrete model for computation. |
45 prover is to formalise a concrete model for computation. |
46 We formalise Turing machines and relate them to abacus machines and recursive |
46 We formalise Turing machines and relate them to abacus machines and recursive |
47 functions. Our theory can be used to formalise other computability results: |
47 functions. Our theory can be used to formalise other computability results: |
48 we give one example about the undecidability of Wang tilings, whose proof uses |
48 we give one example about the undecidability of Wang's tiling problem, whose proof uses |
49 the notion of a universal Turing machine. |
49 the notion of a universal Turing machine. |
50 \end{abstract} |
50 \end{abstract} |
51 |
51 |
52 \begin{IEEEkeywords} |
52 \begin{IEEEkeywords} |
53 Turing Machines, Computability, Isabelle/HOL, Wang tilings |
53 Turing Machines, Computability, Isabelle/HOL, Wang tilings |