A Mechanical Proof of the Unsolvability of the Halting Problem.

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 01, 1982
Accession Number
ADA131731

Entities

People

  • J. Strother Moore
  • Robert S. Boyer

Organizations

  • University of Texas at Austin

Tags

DTIC Thesaurus Topics

  • Automata
  • Computer Languages
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Contracts
  • Formal Languages
  • Governments
  • Language
  • Machines
  • Military Research
  • Procedures (Computers)
  • Programming Languages
  • Recursive Functions
  • United States
  • United States Government

Fields of Study

  • Computer science

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.