Automated Theorem Proving

Inhaltsverzeichnis

• 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.
• 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.