David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
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)|
No categories specified
(categorize this paper)
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library||
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Sara Negri (2011). Proof Analysis: A Contribution to Hilbert's Last Problem. Cambridge University Press.
Paolo Cotogno (2009). A Brief Critique of Pure Hypercomputation. Minds and Machines 19 (3):391-405.
Gabor T. Herman (1969). The Unsolvability of the Uniform Halting Problem for Two State Turing Machines. Journal of Symbolic Logic 34 (2):161-165.
B. Jack Copeland & Oron Shagrir (2011). Do Accelerating Turing Machines Compute the Uncomputable? Minds and Machines 21 (2):221-239.
Verónica Becher & Santiago Figueira (2005). Kolmogorov Complexity for Possibly Infinite Computations. Journal of Logic, Language and Information 14 (2):133-148.
Toby Ord & Tien D. Kieu (2005). The Diagonal Method and Hypercomputation. British Journal for the Philosophy of Science 56 (1):147-156.
Leonard M. Adleman & M. Blum (1991). Inductive Inference and Unsolvability. Journal of Symbolic Logic 56 (3):891-900.
B. Jack Copeland (2002). Accelerating Turing Machines. Minds and Machines 12 (2):281-300.
Herbert A. Simon & Stuart A. Eisenstadt (1998). Human and Machine Interpretation of Expressions in Formal Systems. Synthese 116 (3):439-461.
Added to index2009-01-28
Total downloads9 ( #168,325 of 1,139,853 )
Recent downloads (6 months)1 ( #165,020 of 1,139,853 )
How can I increase my downloads?