A Computational Logic

Half Title......Page 1
Title Page......Page 3
Contents......Page 7
Preface......Page 15
1 Introduction......Page 21
1.1 Motivation......Page 22
1.4 Examples......Page 23
1.5 Our Mechanical Theorem Prover......Page 25
1.6 Artificial Intelligence or Logic?......Page 26
1.7 Organization......Page 27
2.1.1 If and Equal......Page 29
2.1.2 Inductively Constructed Objects......Page 32
2.1.3 Recursively Defined Functions......Page 34
2.1.4 Induction......Page 36
2.2 A Simple Inductive Proof......Page 38
2.3 A More Difficult Problem......Page 40
2.4 A More Difficult Proof......Page 43
2.5 Summary......Page 46
2.6 Notes......Page 47
3.1 Syntax......Page 49
3.2 The Theory of If and Equal......Page 51
3.3 Well-founded Relations......Page 52
3.4 Induction......Page 54
3.5 Shells......Page 57
3.6 Natural Numbers......Page 61
3.7 Literal Atoms......Page 62
3.8 Ordered Pairs......Page 64
3.9 Definitions......Page 65
3.10 Lexicographic Relations......Page 73
3.11 Lessp and Count......Page 74
3.12 Conclusion......Page 77
4 The Correctness of a Tautology Checker......Page 79
4.1 Informal Development......Page 80
4.2.1 Representing Expressions......Page 83
4.2.2 Formal Definitions of Assignment and Value......Page 84
4.2.3 The Formal Correctness Specifications......Page 85
4.3.1 Tautology.checker......Page 86
4.3.2 Summary of the Simple Theorem-proving Ideas......Page 90
4.4.1 Complying With the Principle of Definition......Page 91
4.4.2 Mechanical Proof of Tautology.checker.is.sound......Page 96
4.4.3 Mechanical Proof of Tautology.checker.is.complete......Page 105
4.5 Summary......Page 108
4.6 Notes......Page 110
5.1 The Role of the User......Page 111
5.2 Clausal Representation of Conjectures......Page 112
5.3 The Organization of our Heuristics......Page 113
5.4 The Organization of our Presentation......Page 115
6.1 Type Sets......Page 117
6.2.1 Assuming an Equal-expression True or False......Page 120
6.3.1 The Type Set of a Variable......Page 121
6.3.4 The Type Set of Other Functions......Page 122
6.4.1 Examples of Type Prescriptions......Page 123
6.4.2 Computing the Type Prescription......Page 125
6.6 Notes......Page 127
7.1 Directed Equalities......Page 129
7.2 Infinite Looping......Page 130
7.3 More General Rewrite Rules......Page 131
7.4 An Example of Using Rewrite Rules......Page 133
7.5 Infinite Backwards Chaining......Page 135
7.6 Free Variables In Hypotheses......Page 137
8 Using Definitions......Page 139
8.2 Computing Values......Page 140
8.3 Diving In to See......Page 142
8.3.1 Keeping Nonrecursive Expansions......Page 144
8.3.2 Keeping Recursive Expansions......Page 145
9.1 Rewriting Terms......Page 147
9.1.4 Rewriting Equal-expressions......Page 148
9.1.7 Caveats......Page 150
9.2.1 Converting If-expressions to Clausal Form......Page 151
9.2.2 Caveats......Page 153
9.4 Simplification In the Reverse Example......Page 154
10.1 Trading Bad Terms for Good Terms......Page 159
10.2 The Form of Elimination Lemmas......Page 162
10.3 The Precise Use of Elimination Lemmas......Page 163
10.4 A Nontrivial Example......Page 164
10.5 Multiple Destructors and Infinite Looping......Page 168
10.6 When Elimination Is Risky......Page 169
10.7 Destructor Elimination In the Reverse Example......Page 171
11.1 Using and Throwing Away Equalities......Page 175
11.2 Cross-fertilization......Page 176
11.3 A Simple Example of Cross-fertilization......Page 177
11.4 The Precise Use of Equalities......Page 179
11.5 Cross-fertilization In the Reverse Example......Page 180
12.1 A Simple Generalization Heuristic......Page 183
12.2 Restricting Generalizations......Page 185
12.3 Examples of Generalizations......Page 187
12.4 The Precise Statement of the Generalization Heuristic......Page 188
12.5 Generalization In the Reverse Example......Page 190
13.1 Two Simple Checks for Irrelevance......Page 193
13.2 The Reason for Eliminating Isolated Hypotheses......Page 194
13.3 Elimination of Irrelevance In the Reverse Example......Page 196
14 Induction and the Analysis of Recursive Definitions......Page 197
14.1.1 Machines......Page 199
14.1.2 The Form of Induction Lemmas......Page 201
14.1.3 A Simple Example......Page 203
14.1.4 Lexicographic Measures and Relations......Page 204
14.2 Induction Schemes Suggested By Recursive Functions......Page 206
14.2.1 Why We Use Measures and Relations......Page 207
14.2.2 Measured Subsets......Page 208
14.2.3 Specifying an Induction Schema......Page 210
14.3 The Details of the Definition-time Analysis......Page 216
14.4 Recursion In the Reverse Example......Page 220
15.1.1 Deciding That a Template Applies......Page 221
15.1.2 Obtaining the Induction Scheme Suggested......Page 222
15.1.3 Proof That the Inductions Suggested Are Sound......Page 224
15.2 The Heuristic Manipulation of Induction Schemes......Page 226
15.2.1 Subsumption of Induction Schemes......Page 227
15.2.2 Merging of Induction Schemes......Page 228
15.2.3 Flawed Induction Schemes......Page 231
15.2.4 Tie Breaking Rules......Page 232
15.2.5 Superimposing the Machine......Page 233
15.3 Examples of Induction......Page 234
15.4 The Entire Reverse Example......Page 239
16 Illustrations of our Techniques Via Elementary Number Theory......Page 245
16.1 Plus.right.id......Page 246
16.2 Commutativity2.of.plus......Page 247
16.3 Commutativity.of.plus......Page 251
16.6 Times.zero......Page 255
16.7 Times.add1......Page 256
16.8 Associativity.of.times......Page 259
16.9 Difference......Page 263
16.10 Recursion.by.difference......Page 264
16.12 Quotient......Page 271
16.13 Remainder.quotient.elim......Page 272
17 The Correctness of a Simple Optimizing Expression Compiler......Page 279
17.1 Informal Development......Page 281
17.2.1 The High-level Language......Page 285
17.2.2 The Low-level Language......Page 287
17.3 Formal Definition of the Compiler......Page 291
17.3.2 The Code Generation Pass......Page 292
17.4.1 Decomposition of the Main Goal......Page 294
17.4.2 Proof of the Main Goal......Page 295
17.4.3 Proofs of the Lemmas......Page 296
17.5.1 Bugs Uncovered By the Theorem Prover......Page 307
17.5.2 The History of the Problem......Page 309
18 The Correctness of a Fast String Searching Algorithm......Page 311
18.1.1 The Naive String Searching Algorithm......Page 312
18.1.2 An Example of a Faster Method......Page 313
18.1.3 Preprocessing the Pattern......Page 316
18.1.4 How to Do a Fast String Search......Page 318
18.2.2 The String Matching Problem......Page 321
18.3 Developing the Verification Conditions for the Algorithm......Page 322
18.3.2 Formalizing the Claims......Page 323
18.3.3 Applying the Inductive Assertion Method......Page 326
18.4 The Mechanical Proofs of the Verification Conditions......Page 332
18.4.2 Proof of Fstrpos.vc3......Page 333
18.4.5 Proof of Fstrpos.vc6......Page 334
18.4.6 Proof of Fstrpos.vc7......Page 335
18.4.7 What Have We Proved?......Page 336
18.5.1 Intuitive Simplicity Versus Formal Difficulty......Page 337
18.5.2 Common Misconceptions About the Inductive Assertion Method......Page 338
19.1 The Context......Page 341
19.2 Formal Development of the Unique Prime Factorization Theorem......Page 343
19.2.1 Definition of the Concepts......Page 344
19.2.2 The Statement of the Theorem......Page 346
19.3.1 Elementary Facts About Primes......Page 347
19.3.2 The Existence of a Prime Factorization......Page 351
19.3.3 The Uniqueness of a Prime Factorization......Page 353
A Definitions Accepted and Theorems Proved By our System......Page 361
B The Implementation of the Shell Principle......Page 411
C.1 Logical Definitions......Page 415
C.3 Axioms for Literal Atoms......Page 416
C.5 A Sample Theorem In Clausal Form......Page 417
Index......Page 419
Bibliography......Page 435