Automated theorem proving

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