A Mechanical Proof of the Unsolvability of the Halting Problem
Robert S. Boyer, J Strother Moore · Journal of the ACM · 1984
A proof by a computer program of the unsolvability of the halting problem is described.The halting problem is posed in a construcUve, formal language.The computational paradigm formalized ~s Pure LISP, not Tunng machines.The machine was led to the proof by the authors, who suggested certain function definitions and stated certain intermediate lemmas.The machine checked to ascertain that every suggested definition was admissible and the machine proved the main theorem and every lemma.It is beheved this is the first instance of a machine checking that a given problem is not solvable by machine.