Author | Fitting, Melvin. author |
---|---|
Title | First-Order Logic and Automated Theorem Proving [electronic resource] / by Melvin Fitting |
Imprint | New York, NY : Springer US, 1990 |
Connect to | http://dx.doi.org/10.1007/978-1-4684-0357-2 |
Descript | XV, 242 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 First-Order Uniform Notation -- 5.5 Hintikkaโs Lemma -- 5.6 Parameters -- 5.7 The Model Existence Theorem -- 5.8 Applications -- 5.9 Logical Consequence -- 5.10 Craigโs Interpolation Lemma -- 5.11 Bethโs Definability Theorem -- 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 -- 7.10 The Replacement Theorem -- 7.11 Skolemization -- 7.12 PrenexForm -- 8 Equality -- 8.1 Introduction -- 8.2 Syntax and Semantics -- 8.3 The Equality Axioms -- 8.4 Hintikkaโs Lemma -- 8.5 The Model Existence Theorem -- 8.6 Consequences -- 8.7 Tableau and Resolution Systems -- 8.8 Alternate Tableaux and Resolution Systems -- 8.9 A Free Variable Tableau System With Equality -- 8.10 A Tableaux Implementation With Equality -- 8.11 Paramodulation -- References