Accession Number : AD0619301

Title :   SEMI-AUTOMATED MATHEMATICS: SAM IV.

Descriptive Note : Scientific rept.,

Corporate Author : APPLIED LOGIC CORP PRINCETON N J

Personal Author(s) : BENNETT,James H. ; Easton,William B. ; Guard,James R. ; Loveman,David B. ; Mott,Thomas H. ,Jr.

Report Date : 15 OCT 1964

Pagination or Media Count : 93

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)

Descriptors :   (*MATHEMATICAL LOGIC, THEOREMS), (*COMPUTER PROGRAMMING, MATHEMATICAL LOGIC), COMPUTERS, METAMATHEMATICS, AUTOMATIC

Distribution Statement : APPROVED FOR PUBLIC RELEASE