Proof-Checking, Theorem Proving, and Program Verification.
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1983
- Accession Number
- ADA130638
Entities
People
- J. Strother Moore
- Robert S. Boyer
Organizations
- University of Texas at Austin