1 Background. - 2 Propositional Logic. - 2. 1 Introduction. - 2. 2 Propositional LogicSyntax. - 2. 3 Propositional LogicSemantics. - 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 LogicSyntax. - 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 TheoremConstructively. - 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. Language: English