SEMI-AUTOMATED MATHEMATICS: SAM IV.
Abstract
The fourth in a series of computer experiments on theorem proving is described. The man-machine interactive program is designed to handle any mathematical statement that can be expressed by means of many sorted variables and constants for an omegaorder predicate-function calculus with equality, lambda, and methods of definition. Natural deduction by subordinate proof is used to carry out proofs. The program includes a convenient input/output language, a language for handling sorts and range of symbols, and an automatic logic routine whose function is to automatically justify proof lines which 'trivially' follow from previous results. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 15, 1964
- Accession Number
- AD0619301
Entities
People
- David B. Loveman
- James H. Bennett
- James R. Guard
- Thomas H. Mott Jr.
- William B. Easton