First-Order Logic and Automated Theorem Proving

Springer Science & Business Media, 1996 - Computers - 326 pages
This graduate-level text presents fundamental concepts and results of classical logic in a rigorous mathematical style. Applications to automated theorem proving are considered and usable Prolog programs provided. It will serve both as a first text in formal logic and an introduction to automation issues for students in computer science or mathematics.
The book treats propositional logic, first-order logic, and first-order logic with equality. In each case the initial presentation is semantic, to define the intended subjects independently of the choice of proof mechanism. Then many kinds of proof procedure are introduced. Results such as completeness, compactness, and interpolation are established, and theorem provers are implemented in Prolog. This new edition includes material on AE calculus, Herbrand's Theorem, Gentzen's Theorem, and related topics.

What people are saying -Write a review

We haven't found any reviews in the usual places.

Contents

 Background 1 Prepositional Logic 9 22 Propositional Logic Syntax 10 23 Propositional Logic Semantics 14 24 Boolean Valuations 16 25 The Placement Theorem 20 26 Uniform Notation 23 28 Normal Forms 27
 66 Natural Deduction and Gentzen Sequents 149 Implementing Tableaux and Resolution 151 72 Unification 152 73 Unification Implemented 161 74 FreeVariable Semantic Tableaux 166 75 A Tableau Implementation 169 76 FreeVariable Resolution 184 77 Soundness 188

 29 Normal Form Implementations 35 Semantic Tableaux and Resolution 41 32 Propositional Tableaux Implementations 47 33 Propositional Resolution 51 34 Soundness 55 35 Hintikkas Lemma 58 36 The Model Existence Theorem 59 37 Tableau and Resolution Completeness 64 38 Completeness With Restrictions 69 39 Propositional Consequence 74 Other Propositional Proof Procedures 77 42 Natural Deduction 86 43 The Sequent Calculus 92 44 The DavisPutnam Procedure 98 45 Computational Complexity 104 FirstOrder Logic 109 52 Substitutions 113 53 FirstOrder Semantics 117 54 Herbrand Models 123 55 FirstOrder Uniform Notation 124 56 Hintikkas Lemma 127 57 Parameters 128 58 The Model Existence Theorem 129 59 Applications 132 510 Logical Consequence 135 FirstOrder Proof Procedures 137 62 FirstOrder Resolution 141 63 Soundness 142 64 Completeness 143 65 Hilbert Systems 146
 78 FreeVariable Tableau Completeness 191 79 FreeVariable Resolution Completeness 196 Further FirstOrder Features 203 83 Skolemization 206 84 Prenex Form 209 85 The AECalculus 212 86 Herbrands Theorem 215 87 Herbrands Theorem Constructively 221 88 Gentzens Theorem 225 89 Cut Elimination 228 810 Do Cuts Shorten Proofs? 243 811 Craigs Interpolation Theorem 254 812 Craigs Interpolation TheoremConstructively 257 813 Beths Definability Theorem 263 814 Lyndons Homomorphism Theorem 266 Equality 271 92 Syntax and Semantics 273 93 The Equality Axioms 276 94 Hintikkas Lemma 279 95 The Model Existence Theorem 284 96 Consequences 285 97 Tableau and Resolution Systems 288 98 Alternate Tableau and Resolution Systems 294 99 A FreeVariable Tableau System With Equality 298 910 A Tableau Implementation With Equality 305 911 Paramodulation 312 References 315 Index 319 Copyright

Popular passages

Page 326 - Gentzen sequents and axiom systems. Completeness issues are centered in a Model Existence Theorem, which permits the coverage of a variety of proof procedures without repetition of detail. In addition, results such as Compactness, Interpolation, and the Beth Definability theorem are easily established. Implementations of tableau theorem provers are given in Prolog, and resolution is left as a project for the student.
Page 316 - Toward mechanical mathematics. IBM Journal for Research and Development 4 (1960). Reprinted in A Survey of Mathematical Logic.
Page 326 - This monograph on classical logic presents fundamental concepts and results in a rigorous mathematical style. Applications to automated theorem proving are considered and usable programs in Prolog are provided. This material can be used both as a first text in formal logic and as an introduction to automation issues, and is intended for those interested in computer science and mathematics at the beginning graduate level. The book begins with propositional logic, then treats first-order logic, and...
Page 315 - LJ N-sorted logic for automatic theorem proving in higher-order logic. Proc. ACM '72 Conf., pp. 71-81. 3. Henschen, LJ, and Wos, L. Unit refutations and horn sets. J. ACM (to appear). 4. Robinson, G., and Wos, L. Paramodulation and theorem proving in first-order theories with equality. In Machine Intelligence, Vol. 4, B. Meltzer and D. Michie, Eds., American Elsevier, New York, 1969, pp.
Page 315 - SMULLYAN, RM Trees and ball games. Annals of the New York Academy of Sciences 321 (1979), 86-90.