Report
Proof-checking, theorem proving and program verification
Proof-checking, theorem proving and program verification, pp.23P-23P
01 May 1983
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' 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.
Metrics
2 Record Views
Details
- Title
- Proof-checking, theorem proving and program verification
- Creators
- R BoyerJ Moore
- Publication Details
- Proof-checking, theorem proving and program verification, pp.23P-23P
- Resource Type
- Report
- Language
- English
- Academic Unit
- [Retired Faculty]; Mathematics
- Identifiers
- 991020638507904721