TOWARD SEMI-AUTOMATED MATHEMATICS: THE LANGUAGE AND LOGIC OF SAM III.
Scientific rept. no. 2,
APPLIED LOGIC CORP PRINCETON N J
Pagination or Media Count:
This report describes the third in a series of computer experiments designed to explore the extent to which computers may feasibly be used in doing formal mathematics. All the experiments are based on and employ principles of man-machine interaction. The first two, dubbed SAM I and SAM II, are described in an earlier report AD-413 929. They consist of a source language, closely resembling the language of mathematical logic, and an associated machine language processor for specifying exact procedures for building proofs in elementary natural deductive and first-order axiom systems of mathematics such as the propositional calculus, elementary group theory and set theory. The third program, described in this report, represents an attempt to extend the capabilities of these programs to handle more advanced systems of mathematics. Dubbed SAM III, the program includes the salient features of SAM I and SAM II but, in addition, contains provisions for the introduction of quantification theory, inference by substitution for variables of finite, mixed types, automatic application of rules of propositional and equality inference, and other important features. Natural deduction is retained as the basic method for carrying out proofs in the system. Author