We describe a proof by a computer program of the unsolvability of the halting problem. The halting problem is posed in a constructive, formal language. The computational paradigm formalized is Pure LISP, not Turing machines. The machine was led to the proof by the authors, who suggested certain function definitions and stated certain intermediate lemmas. The machine checked that every suggested definition was admissible and the machine proved the main theorem and every lemma. We believe this is the first instance of a machine checking that a given problem is not solvable by machine.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
The Unsolvability of the Uniform Halting Problem for Two State Turing Machines.Gabor T. Herman - 1969 - Journal of Symbolic Logic 34 (2):161-165.
Kolmogorov Complexity for Possibly Infinite Computations.Verónica Becher & Santiago Figueira - 2005 - Journal of Logic, Language and Information 14 (2):133-148.
The Diagonal Method and Hypercomputation.Toby Ord & Tien D. Kieu - 2005 - British Journal for the Philosophy of Science 56 (1):147-156.
Inductive Inference and Unsolvability.Leonard M. Adleman & M. Blum - 1991 - Journal of Symbolic Logic 56 (3):891-900.
Human and Machine Interpretation of Expressions in Formal Systems.Herbert A. Simon & Stuart A. Eisenstadt - 1998 - Synthese 116 (3):439-461.
Added to index2009-01-28
Total downloads27 ( #185,115 of 2,152,538 )
Recent downloads (6 months)1 ( #399,788 of 2,152,538 )
How can I increase my downloads?