Author | Fitting, Melvin. author |
---|---|
Title | First-Order Logic and Automated Theorem Proving [electronic resource] / by Melvin Fitting |
Imprint | New York, NY : Springer New York, 1996 |
Edition | Second Edition |
Connect to | http://dx.doi.org/10.1007/978-1-4612-2360-3 |
Descript | XVIII, 326 p. online resource |
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