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