Automated Theorem Proving

I. Natural and formal logic.- 1. Logic abstracted from natural reasoning.- 2. Logical rules.- II. The connection method in propositional logic.- 1. The language of propositional logic.- 2. The semantics of propositional logic.- 3. A basic syntactic characterization of validity.- 4. The connection calculus.- 5. Consistency, completeness, and confluence.- 6. Algorithmic aspects.- 7. Exercises.- 8. Bibliographical and historical remarks.- III. The connection method in first-order logic.- 1. The language of first-order logic.- 2. The semantics of first-order logic.- 3. A basic syntactic characterization of validity.- 4. Transformation to normal form.- 5. Unification.- 6. The connection calculus.- 7. Algorithmic aspects.- 8. Exercises.- 9. Bibliographical and historical remarks.- IV. Variants and improvements.- 1. Resolution.- 2. Linear resolution and the connection method.- 3. On performance evaluation.- 4. Connection graph resolution and the connection method.- 5. A connection procedure for arbitrary matrices.- 6. Reduction, factorization, and tautological circuits.- 7. Logical calculi of natural deduction.- 8. An alternative for skolemization.- 9. Linear unification.- 10. Splitting by need.- 11. Summary and prospectus.- 12. Exercises.- 13. Bibliographical and historical remarks.- V. Applications and extensions.- 1. Structuring and processing knowledge.- 2. Programming and problem solving.- 3. The connection method with equality.- 4. Rewrite rules and generalized unification.- 5. The connection method with induction.- 6. The connection method in higher-order logic.- 7. Aspects of actual implementations.- 8. Omissions.- 9. Exercises.- 10. Bibliographical and historical remarks.- References.- List of Symbols.