AUTOMATED LOGIC FOR SEMI-AUTOMATED MATHEMATICS
Abstract
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 Gentzen's treatment by Sequenzen in that Gentzen's '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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 30, 1964
- Accession Number
- AD0602710
Entities
People
- James R. Guard