AUTOMATED LOGIC FOR SEMI-AUTOMATED MATHEMATICS
Scientific rept. no. 1
APPLIED LOGIC CORP PRINCETON NJ
Pagination or Media Count:
This report defines and describes six formal systems of logic, S sub 1 through S sub 6, for which proof procedures or partial proof procedures are readily contrived. The systems S sub 1 through S sub 4 are considered in order to simplify the descriptions of S sub 5 and S sub 6. System S sub 1 is a fragment of the classical propositional calculus whose theorems are those tautologies which can be shown tautologous by assuming them to take on the value falsehood and arriving at an inconsistent assignment to the variables by not using any branching rules. This system suggests an efficient means of handling the propositional connectives in the later systems. System S sub 2 is the completion of S sub 1. S sub 2 has branching rules which correspond to treating certain propositional variables by cases. This differs from Gentzens treatment by Sequenzen in that Gentzens branching rules consider the value of the antecedent or consequent of a formula by cases. System S sub 3 is a fragment of the first order predicate-function calculus. In S sub 3, formulas are proved by contradiction. The quantifiers of the denial are stripped by putting the denial in miniscope form and replacing them by Skolem functors. This is reminiscent of the Herbrand technique. However S sub 3 uses a process called matching to consider only reasonable Herbrand disjuncts.
- Computer Programming and Software