
Accession Number : AD0619301
Title : SEMIAUTOMATED 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 manmachine interactive program is designed to handle any mathematical statement that can be expressed by means of many sorted variables and constants for an omegaorder predicatefunction 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