First-Order Logic and Automated Theorem Proving

Front Cover
Springer Science & Business Media, 1996 - Computers - 326 pages
1 Review
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

Common terms and phrases

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.

References to this book

All Book Search results »

Bibliographic information