First-Order Logic and Automated Theorem Proving

1 Background.- 2 Propositional Logic.- 2.1 Introduction.- 2.2 Propositional Logic-Syntax.- 2.3 Propositional Logic-Semantics.- 2.4 Boolean Valuations.- 2.5 The Replacement Theorem.- 2.6 Uniform Notation.- 2.7 König's Lemma.- 2.8 Normal Forms.- 2.9 Normal Form Implementations.- 3 Semantic Tableaux and Resolution.- 3.1 Propositional Semantic Tableaux.- 3.2 Propositional Tableaux Implementations.- 3.3 Propositional Resolution.- 3.4 Soundness.- 3.5 Hintikka's Lemma.- 3.6 The Model Existence Theorem.- 3.7 Tableau and Resolution Completeness.- 3.8 Completeness With Restrictions.- 3.9 Propositional Consequence.- 4 Other Propositional Proof Procedures.- 4.1 Hilbert Systems.- 4.2 Natural Deduction.- 4.3 The Sequent Calculus.- 4.4 The Davis-Putnam Procedure.- 4.5 Computational Complexity.- 5 First-Order Logic.- 5.1 First-Order Logic-Syntax.- 5.2 Substitutions.- 5.3 First-Order Semantics.- 5.4 Herbrand Models.- 5.5 First-Order Uniform Notation.- 5.6 Hintikka's Lemma.- 5.7 Parameters.- 5.8 The Model Existence Theorem.- 5.9 Applications.- 5.10 Logical Consequence.- 6 First-Order Proof Procedures.- 6.1 First-Order Semantic Tableaux.- 6.2 First-Order Resolution.- 6.3 Soundness.- 6.4 Completeness.- 6.5 Hilbert Systems.- 6.6 Natural Deduction and Gentzen Sequents.- 7 Implementing Tableaux and Resolution.- 7.1 What Next.- 7.2 Unification.- 7.3 Unification Implemented.- 7.4 Free-Variable Semantic Tableaux.- 7.5 A Tableau Implementation.- 7.6 Free-Variable Resolution.- 7.7 Soundness.- 7.8 Free-Variable Tableau Completeness.- 7.9 Free-Variable Resolution Completeness.- 8 Further First-Order Features.- 8.1 Introduction.- 8.2 The Replacement Theorem.- 8.3 Skolemization.- 8.4 Prenex Form.- 8.5 The AE-Calculus.- 8.6 Herbrand's Theorem.- 8.7 Herbrand's Theorem, Constructively.- 8.8 Gentzen's Theorem.- 8.9 Cut Elimination.- 8.10 Do Cuts Shorten Proofs?.- 8.11 Craig's Interpolation Theorem.- 8.12 Craig's Interpolation Theorem-Constructively.- 8.13 Beth's Definability Theorem.- 8.14 Lyndon's Homomorphism Theorem.- 9 Equality.- 9.1 Introduction.- 9.2 Syntax and Semantics.- 9.3 The Equality Axioms.- 9.4 Hintikka's Lemma.- 9.5 The Model Existence Theorem.- 9.6 Consequences.- 9.7 Tableau and Resolution Systems.- 9.8 Alternate Tableau and Resolution Systems.- 9.9 A Free-Variable Tableau System With Equality.- 9.10 A Tableau Implementation With Equality.- 9.11 Paramodulation.- References.