CRT-AIDED SEMI-AUTOMATED MATHEMATICS
Final rept. 1 Jun 1963-30 Sep 1966
APPLIED LOGIC CORP PRINCETON NJ
Pagination or Media Count:
The report describes the status of the fifth in a series of five experiments in semi-automated mathematics. These experiments culminated in large complex computer programs which allow a mathematician to prove mathematical theorems on a man-machine basis. SAM V, the fifth 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 V. These include IO 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 an auto-logic algorithm and matching routine. The latter constitute the capability for handling, automatically, logic with equality. This capability is particularly useful at an intermediate state of the proof when it is desired to have the machine try and verify automatically a given portion of the proof.
- Theoretical Mathematics
- Computer Programming and Software
- Computer Hardware