Boyer / Moore / Standish A Computational Logic

1. Auflage 2014
ISBN: 978-1-4832-7788-2
Verlag: Elsevier Science & Techn.
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 414 Seiten, Web PDF

ACM Monograph Series: A Computational Logic focuses on the use of induction in proving theorems, including the use of lemmas and axioms, free variables, equalities, and generalization. The publication first elaborates on a sketch of the theory and two simple examples, a precise definition of the theory, and correctness of a tautology-checker. Topics include mechanical proofs, informal development, formal specification of the problem, well-founded relations, natural numbers, and literal atoms. The book then examines the use of type information to simplify formulas, use of axioms and lemmas as rewrite rules, and the use of definitions. Topics include nonrecursive functions, computing values, free variables in hypothesis, infinite backwards chaining, infinite looping, computing type sets, and type prescriptions. The manuscript takes a look at rewriting terms and simplifying clauses, eliminating destructors and irrelevance, using equalities, and generalization. Concerns include reasons for eliminating isolated hypotheses, precise statement of the generalization heuristic, restricting generalizations, precise use of equalities, and multiple destructors and infinite looping. The publication is a vital source of data for researchers interested in computational logic.

Autoren/Hrsg.

Boyer, Robert S.

Moore, J Strother

Standish, Thomas A.

Inhaltsverzeichnis

1;Front Cover;1
2;A Computational Logic;4
3;Copyright Page;5
4;Table of Contents;8
5;Dedication;6
6;Preface;12
7;Chapter 1. Introduction;16
7.1;A. Motivation;17
7.2;B. Our Formal Theory;17
7.3;C. Proof Techniques;18
7.4;D. Examples;18
7.5;E. Our Mechanical Theorem-Prover;19
7.6;F. Artificial Intelligence or Logic?;21
7.7;G. Organization;21
8;Chapter 2. A Sketch of the Theory and Two Simple Examples;23
8.1;A. An Informal Sketch of the Theory;23
8.2;B. A Simple Inductive Proof;31
8.3;C. A More Difficult Problem;34
8.4;D. A More Difficult Proof;36
8.5;E. Summary;41
8.6;F. Notes;41
9;Chapter 3. A Precise Definition of the Theory;43
9.1;A. Syntax;43
9.2;B. The Theory of IF and EQUAL;45
9.3;C. Well-Founded Relations;46
9.4;D. Induction;48
9.5;E. Shells;50
9.6;F. Natural Numbers;55
9.7;G. Literal Atoms;56
9.8;H. Ordered Pairs;57
9.9;I. Definitions;58
9.10;J. Lexicographic Relations;66
9.11;K. LESSP and COUNT;67
9.12;L. Conclusion;70
10;Chapter 4. The Correctness of a Tautology-Checker;71
10.1;A. Informal Development;72
10.2;B. Formal Specification of the Problem;74
10.3;C. The Former Definition of TAUTOLOGY.CHECKER;78
10.4;D. The Mechanical Proofs;82
10.5;E. Summary;99
10.6;F. Notes;100
11;Chapter 5. An Overview of How We Prove Theorems;102
11.1;A. The Role of the User;102
11.2;B. Clausal Representation of Conjectures;103
11.3;C. The Organization of Our Heuristics;104
11.4;D. The Organization of Our Presentation;106
12;Chapter 6. Using Type Information to Simplify Formulas;107
12.1;A. Type Sets;107
12.2;B. Assuming Expressions True or False;110
12.3;C. Computing Type Sets;111
12.4;D. Type Prescriptions;112
12.5;E. Summary;116
12.6;F. Notes;117
13;Chapter 7. Using Axioms and Lemmas as Rewrite Rules;118
13.1;A. Directed Equalities;118
13.2;B. Infinite Looping;119
13.3;C. More General Rewrite Rules;120
13.4;D. An Example of Using Rewrite Rules;122
13.5;E. Infinite Backwards Chaining;124
13.6;F. Free Variables in Hypotheses;126
14;Chapter 8. Using Definitions;128
14.1;A. Nonrecursive Functions;129
14.2;B. Computing Values;129
14.3;C. Diving in to See;131
15;Chapter 9. Rewriting Terms and Simplifying Clauses;135
15.1;A. Rewriting Terms;135
15.2;B. Simplifying Clauses;139
15.3;C. The REVERSE Example;141
15.4;D. Simplification in the REVERSE Example;142
16;Chapter 10. Eliminating Destructors;145
16.1;A. Trading Bad Terms for Good Terms;145
16.2;B. The Form of Elimination Lemmas;148
16.3;C. The Precise Use of Elimination Lemmas;149
16.4;D. A Nontrivial Example;150
16.5;E. Multiple Destructors and Infinite Looping;154
16.6;F. When Elimination Is Risky;154
16.7;G. Destructor Elimination in the REVERSE Example;156
17;Chapter 11. Using Equalities;160
17.1;A. Using and Throwing Away Equalities;160
17.2;B. Cross-Fertilization;161
17.3;C. A Simple Example of Cross-Fertilization;162
17.4;D. The Precise Use of Equalities;164
17.5;E. Cross-Fertilization in the REVERSE Example;165
18;Chapter 12. Generalization;166
18.1;A. A Simple Generalization Heuristic;166
18.2;B. Restricting Generalizations;168
18.3;C. Examples of Generalizations;169
18.4;D. The Precise Statement of the Generalization Heuristic;171
18.5;E. Generalization in the REVERSE Example;172
19;Chapter 13. Eliminating Irrelevance;174
19.1;A. Two Simple Checks for Irrelevance;174
19.2;B. The Reason for Eliminating Isolated Hypotheses;175
19.3;C. Elimination of Irrelevance in the REVERSE Example;177
20;Chapter 14. Induction and the Analysis of Recursive Definitions;178
20.1;A. Satisfying the Principle of Definition;179
20.2;B. Induction Schemes Suggested by Recursive Functions;186
20.3;C. The Details of the Definition-Time Analysis;195
20.4;D. Recursion in the REVERSE Example;198
21;Chapter 15. Formulating an Induction Scheme for a Conjecture;200
21.1;A. Collecting the Induction Candidates;200
21.2;B. The Heuristic Manipulation of Induction Schemes;204
21.3;C. Examples of Induction;212
21.4;D. The Entire REVERSE Example;217
22;Chapter 16. Illustrations of Our Techniques via Elementary Number Theory;224
22.1;A. PLUS.RIGHT.ID;224
22.2;B. COMMUTATIVITY2.OF.PLUS;226
22.3;C. COMMUTATIVITY.OF.PLUS;231
22.4;D. ASSOCIATIVITY.OF.PLUS;236
22.5;E. TIMES;236
22.6;F. TIMES.ZERO;237
22.7;G. TIMES.ADD1;238
22.8;H. ASSOCIATIVITY.OF.TIMES;242
22.9;I. DIFFERENCE;248
22.10;J. RECURSION.BY.DIFFERENCE;248
22.11;K. REMAINDER;257
22.12;L. QUOTIENT;257
22.13;M. REMAINDER.QUOTIENT.ELIM;258
23;Chapter 17. The Correctness of a Simple Optimizing Expression Compiler;267
23.1;A. Informal Development;268
23.2;B. Formal Specification of the Problem;272
23.3;C. Formal Definition of the Compiler;278
23.4;D. The Mechanical Proof of Correctness;281
23.5;E. Notes;294
24;Chapter 18. The Correctness of a Fast String Searching Algorithm;297
24.1;A. Informal Development;298
24.2;B. Formal Specification of the Problem;306
24.3;C. Developing the Verification Conditions for the Algorithm;307
24.4;D. The Mechanical Proofs of the Verification Conditions;316
24.5;E. Notes;320
25;Chapter 19. The Unique Prime Factorization Theorem;324
25.1;A. The Context;324
25.2;B. Formal Development of the Unique Prime Factorization Theorem;326
25.3;C. The Mechanical Proofs;330
26;Appendix A: Definitions Accepted and Theorems Proved by Our System;344
27;Appendix B: The Implementation of the Shell Principle;391
28;Appendix C: Clauses for Our Theory;395
29;References;400
30;Index;404