Accession Number : ADA131731

Title :   A Mechanical Proof of the Unsolvability of the Halting Problem.

Descriptive Note : Technical rept.,

Corporate Author : TEXAS UNIV AT AUSTIN INST FOR COMPUTING SCIENCE AND COMPUTER APPLICATIONS

Personal Author(s) : Boyer,Robert S ; Moore,J Strother

PDF Url : ADA131731

Report Date : Jul 1982

Pagination or Media Count : 30

Abstract : The authors 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. They believe this is the first instance of a machine proving that a given problem is not solvable by machine.

Descriptors :   *Computer logic, *Problem solving, *Computer program verification, Programming languages, Interpreters, Computations, Recursive functions, Semantics

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE