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