## First-Order Logic and Automated Theorem ProvingThere 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 |

315 | |

319 | |

### Other editions - View all

### Common terms and phrases

algorithm applied assignment Atomic Closure atomic formula automated theorem proving Axiom Scheme binary Boolean valuation branch closure clause set closed tableau closed term completeness conjunction constant symbol contains defined Definition disjunction domain Dual Clause Form equality Exercise finite subset first-order consistency property first-order language first-order logic free variables free-variable tableau function symbol hence Hilbert system Hintikka's Lemma implementation infinite interpolant Lpar Model Existence Theorem Modus Ponens natural deduction negation node normal model notation notion P D Q parameter Prolog proof procedures property Q propositional formula propositional letters propositional logic prove Q D R quantifiers RDepth relation symbol Resolution Expansion Rules resolution proof Resolution Rule result Rule applications satisfiable Section semantic sequent calculus Skolem function structural induction subformula substitution Suppose tableau construction Tableau Expansion Rule tableau proof tableau system tautology theorem provers true unification unifier valid X D Y

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