Accession Number : ADA130638

Title :   Proof-Checking, Theorem Proving, and Program Verification.

Descriptive Note : Techncial 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 : ADA130638

Report Date : Jan 1983

Pagination or Media Count : 23

Abstract : This article consists of three parts: a tutorial introduction to a computer program that proves theorems by induction; a brief description of recent applications of that theorem-prover; and a discussion of several nontechnical aspects of the problem of building automatic theorem-provers. The theorem-prover described has proved such theorems as the uniqueness of prime factorizations, Fermat's theorem, and the recursive unsolvability of the halting problem. The article is aimed at those who know nothing about automatic theorem-proving but would like a glimpse of one such system. The authors' in opinion, the limiting factor in progress in automatic theorem-proving is the quality of the mathematicians who are attempting to build such systems. They encourage good mathematicians to work in the field.

Descriptors :   *Theorems, *Computer program verification, Recursive functions, Heuristic methods, Algorithms, Fortran, Decision making, Logic

Subject Categories : Theoretical Mathematics
      Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE