CRT-AIDED SEMI-AUTOMATED MATHEMATICS
James H. Bennett, William B. Easton, James R. Guard, L. G. Settle · 1967
The report describes the status of the sixth in a series of six experiments in semi-automated mathematics. These experiments culminated in large complex computer programs that allow a mathematician to prove mathematical theorems on a man-machine basis. SAM VI, the sixth program, uses a cathode ray tube as the principal interface between the mathematician and a high speed digital computer. An elaborate language and logical capability has been implemented in SAM VI. These include 1/10 languages for expressing mathematical statements in a form suitable for both the mathematician and the machine to recognize and handle with ease and convenience, a language for expressing and handling sorts and range of symbols, and auto-logic alogirthm and matching routine. The latter contain the capability for handling, automatically, logic with equality.