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

315 | |

319 | |

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