Accession Number:

AD0619301

Title:

SEMI-AUTOMATED MATHEMATICS: SAM IV.

Descriptive Note:

Scientific rept.,

Corporate Author:

APPLIED LOGIC CORP PRINCETON N J

Report Date:

1964-10-15

Pagination or Media Count:

93.0

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 inputoutput 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

Subject Categories:

Distribution Statement:

APPROVED FOR PUBLIC RELEASE