Symbolic Logic and Mechanical Theorem Proving (eBook)

Front Cover 
1 
Symbolic Logic and 
4 
Copyright Page 5
Table of 
8 
Dedication 6
Preface 12
Acknowledgments 14
Chapter 
18 
1.1 Artificial Intelligence, Symbolic Logic, and Theorem Proving 18
1.2 Mathematical Background 21
References 22
Chapter 
23 
2.1 Introduction 23
2.2 Interpretations of Formulas in the Propositional Logic 25
2.3 Validity and Inconsistency in the Propositional Logic 27
2.4 Normal Forms in the Propositional 
29 
2.5 Logical Consequences 32
2.6 Applications of the Propositional Logic 36
References 40
Exercises 40
Chapter 
43 
3.1 Introduction 43
3.2 Interpretations of Formulas in the First-Order Logic 47
3.3 Prenex Normal Forms in the First-Order Logic 52
3.4 Applications of the First-Order 
56 
References 58
Exercises 58
Chapter 
62 
4.1 Introduction 62
4.2 Skolem Standard Forms 63
4.3 The Herbrand Universe of a Set of Clauses 68
4.4 Semantic Trees 73
4.5 Herbrand's 
77 
4.6 Implementation of Herbrand's Theorem 79
References 83
Exercises 84
Chapter 
87 
5.1 Introduction 87
5.2 The Resolution Principle for the Propositional Logic 88
5.3 Substitution and Unification 91
5.4 Unification Algorithm 94
5.5 The Resolution Principle for the First-Order Logic 97
5.6 Completeness of the Resolution Principle 100
5.7 Examples Using the Resolution 
103 
5.8 Deletion Strategy 109
References 114
Exercises 114
Chapter 
117 
6.1 Introduction 117
6.2 An Informal Introduction to Semantic Resolution 118
6.3 Formal Definitions and Examples of Semantic Resolution 121
6.4 Completeness of Semantic Resolution 123
6.5 Hyperresolution and the Set-of-Support Strategy: Special Cases of Semantic Resolution 124
6.6 Semantic Resolution Using Ordered Clauses 128
6.7 Implementation of Semantic Resolution 134
6.8 Lock Resolution 137
6.9 Completeness of Lock 
141 
References 142
Exercises 143
Chapter 
147 
7.1 Introduction 147
7.2 Linear Resolution 148
7.3 Input Resolution and Unit Resolution 149
7.4 Linear Resolution Using 
152 
7.5 Completeness of Linear Resolution 159
7.6 Linear Deduction and Tree 
162 
7.7 Heuristics in Tree Searching 169
7.8 Estimations of Evaluation Functions 171
References 175
Exercises 176
Chapter 
180 
8.1 Introduction 180
8.2 Unsatisfiability under Special Classes of Models 182
8.3 Paramodulation—An Inference Rule for Equality 185
8.4 Hyperparamodulation 187
8.5 Input and Unit Paramodulations 190
8.6 Linear Paramodulation 195
References 197
Exercises 198
Chapter 
201 
9.1 Introduction 201
9.2 The Prawitz Procedure 202
9.3 The V-Resolution Procedure 206
9.4 Pseudosemantic Trees 214
9.5 A Procedure for Generating Closed Pseudosemantic Trees 216
9.6 A Generalization of the Splitting Rule of Davis and Putnam 222
References 224
Exercises 225
Chapter 
227 
10.1 Introduction 227
10.2 An Informal Discussion 228
10.3 Formal Définitions of Programs 230
10.4 Logical Formulas Describing the Execution of a Program 233
10.5 Program Analysis by Resolution 234
10.6 The Termination and Response of Programs 239
10.7 The Set-of-Support Strategy and the Deduction of the Halting Clause 242
10.8 The Correctness and Equivalence of Programs 244
10.9 The Specialization of Programs 245
References 248
Exercises 249
Chapter 11. Deductive Question Answering, Problem Solving, and Program Synthesis 251
11.1 Introduction 251
11.2 Class A Questions 253
11.3 Class B Questions 254
11.4 Class C Questions 257
11.5 Class D Questions 260
11.6 Completeness of Resolution for Deriving Answers 267
11.7 The Principles of Program Synthesis 268
11.8 Primitive Resolution and Algorithm A 
275 
11.9 The Correctness of Algorithm 
284 
11.10 The Application of Induction Axioms to Program Synthesis 288
11.11 Algorithm A (An Improved Program-Synthesizing Algorithm 292
References 296
Exercises 297
Chapter 
300 
References 301
Appendix A 304
A.l A Computer Program Using Unit Binary Resolution 304
A.2 Brief Comments on the Program 307
A.3 A Listing of the Program 309
A.4 Illustrations 315
References 322
Appendix B 323
Bibliography 326
INDEX 342