# First-Order Logic and Automated Theorem Proving

Springer Science & Business Media, 1996 - Computers - 326 pages
There are many kinds of books on formal logic. Some have philosophers as their intended audience, some mathematicians, some computer scien tists. Although there is a common core to all such books, they will be very different in emphasis, methods, and even appearance. This book is intended for computer scientists. But even this is not precise. Within computer science formal logic turns up in a number of areas, from pro gram verification to logic programming to artificial intelligence. This book is intended for computer scientists interested in automated theo rem proving in classical logic. To be more precise yet, it is essentially a theoretical treatment, not a how-to book, although how-to issues are not neglected. This does not mean, of course, that the book will be of no interest to philosophers or mathematicians. It does contain a thorough presentation of formal logic and many proof techniques, and as such it contains all the material one would expect to find in a course in formal logic covering completeness but, not incompleteness issues. The first item to be addressed is, What are we talking about and why are we interested in it? We are primarily talking about truth as used in mathematical discourse, and our interest in it is, or should be, self evident. Truth is a semantic concept, so we begin with models and their properties. These are used to define our subject.

### 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.