SEMI-AUTOMATED MATHEMATICS: SAM IV.
APPLIED LOGIC CORP PRINCETON N J
Pagination or Media Count:
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