
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