INTRODUCTION TO SEMI-AUTOMATED MATHEMATICS.
Abstract
The subject of this report is mechanical theorem proving, and in it are described two computer programs that represent an approach different from the usual ones based on the Herbrand Theorem in which the computer unaided seeks to construct proofs. In the approach described here, non algorithmic proof procedures are employed and the basic function of the computer is to render as much assistance as possible to the mathe matician in specifying such procedures. To aid in this function, two programming languages and associated processors have been written that pro vide a logical language, closely resembling the language of mathematical logic, for specifying to the computer exact procedures for building proofs in the propositional calculus and first order axioms systems. One language is based on a natural deduction formulation of the proposi tional calculus, and the other on an axiomatic formulation of any first-order axiom system such as elementary group theory and set theory. Among the provisions of the latter language is a com mand for generating the most general relevant substitution instances of axioms and theorems already proved. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 15, 1963
- Accession Number
- AD0413929
Entities
People
- James H. Bennett
- James R. Guard
- Thomas H. Mott Jr.
- William B. Easton