Chang / Lee Symbolic Logic and Mechanical Theorem Proving

1. Auflage 2014
ISBN: 978-0-08-091728-3
Verlag: Elsevier Science & Techn.
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 331 Seiten, Web PDF

This book contains an introduction to symbolic logic and a thorough discussion of mechanical theorem proving and its applications. The book consists of three major parts. Chapters 2 and 3 constitute an introduction to symbolic logic. Chapters 4-9 introduce several techniques in mechanical theorem proving, and Chapters 10 an 11 show how theorem proving can be applied to various areas such as question answering, problem solving, program analysis, and program synthesis.

Zielgruppe

Adult: General

Autoren/Hrsg.

Chang, Chin-Liang

Lee, Richard Char-Tung

Inhaltsverzeichnis

1;Front Cover
;1
2;Symbolic Logic and
Mechanical Theorem Proving;4
3;Copyright Page;5
4;Table of
Contents;8
5;Dedication;6
6;Preface;12
7;Acknowledgments;14
8;Chapter
1. Introduction;18
8.1;1.1 Artificial Intelligence, Symbolic Logic, and Theorem Proving;18
8.2;1.2 Mathematical Background;21
8.3;References;22
9;Chapter
2. The Propositional Logic;23
9.1;2.1 Introduction;23
9.2;2.2 Interpretations of Formulas in the Propositional Logic;25
9.3;2.3 Validity and Inconsistency in the Propositional Logic;27
9.4;2.4 Normal Forms in the Propositional
Logic;29
9.5;2.5 Logical Consequences;32
9.6;2.6 Applications of the Propositional Logic;36
9.7;References;40
9.8;Exercises;40
10;Chapter
3. The First-Order Logic;43
10.1;3.1 Introduction;43
10.2;3.2 Interpretations of Formulas in the First-Order Logic;47
10.3;3.3 Prenex Normal Forms in the First-Order Logic;52
10.4;3.4 Applications of the First-Order
Logic;56
10.5;References;58
10.6;Exercises;58
11;Chapter
4. Herbrand's Theorem;62
11.1;4.1 Introduction;62
11.2;4.2 Skolem Standard Forms;63
11.3;4.3 The Herbrand Universe of a Set of Clauses;68
11.4;4.4 Semantic Trees;73
11.5;4.5 Herbrand's
Theorem;77
11.6;4.6 Implementation of Herbrand's Theorem;79
11.7;References;83
11.8;Exercises;84
12;Chapter
5. The Resolution Principle;87
12.1;5.1 Introduction;87
12.2;5.2 The Resolution Principle for the Propositional Logic;88
12.3;5.3 Substitution and Unification;91
12.4;5.4 Unification Algorithm;94
12.5;5.5 The Resolution Principle for the First-Order Logic;97
12.6;5.6 Completeness of the Resolution Principle;100
12.7;5.7 Examples Using the Resolution
Principle;103
12.8;5.8 Deletion Strategy;109
12.9;References;114
12.10;Exercises;114
13;Chapter
6. Semantic Resolution and Lock Resolution;117
13.1;6.1 Introduction;117
13.2;6.2 An Informal Introduction to Semantic Resolution;118
13.3;6.3 Formal Definitions and Examples of Semantic Resolution;121
13.4;6.4 Completeness of Semantic Resolution;123
13.5;6.5 Hyperresolution and the Set-of-Support Strategy: Special Cases of Semantic Resolution;124
13.6;6.6 Semantic Resolution Using Ordered Clauses;128
13.7;6.7 Implementation of Semantic Resolution;134
13.8;6.8 Lock Resolution;137
13.9;6.9 Completeness of Lock
Resolution;141
13.10;References;142
13.11;Exercises;143
14;Chapter
7. Linear Resolution;147
14.1;7.1 Introduction;147
14.2;7.2 Linear Resolution;148
14.3;7.3 Input Resolution and Unit Resolution;149
14.4;7.4 Linear Resolution Using
Ordered Clauses and the Information of Resolved Literals;152
14.5;7.5 Completeness of Linear Resolution;159
14.6;7.6 Linear Deduction and Tree
Searching;162
14.7;7.7 Heuristics in Tree Searching;169
14.8;7.8 Estimations of Evaluation Functions;171
14.9;References;175
14.10;Exercises;176
15;Chapter
8. The Equality Relation;180
15.1;8.1 Introduction;180
15.2;8.2 Unsatisfiability under Special Classes of Models;182
15.3;8.3 Paramodulation—An Inference Rule for Equality;185
15.4;8.4 Hyperparamodulation;187
15.5;8.5 Input and Unit Paramodulations;190
15.6;8.6 Linear Paramodulation;195
15.7;References;197
15.8;Exercises;198
16;Chapter
9. Some Proof Procedures Based on Herbrand's Theorem;201
16.1;9.1 Introduction;201
16.2;9.2 The Prawitz Procedure;202
16.3;9.3 The V-Resolution Procedure;206
16.4;9.4 Pseudosemantic Trees;214
16.5;9.5 A Procedure for Generating Closed Pseudosemantic Trees;216
16.6;9.6 A Generalization of the Splitting Rule of Davis and Putnam;222
16.7;References;224
16.8;Exercises;225
17;Chapter
10. Program Analysis;227
17.1;10.1 Introduction;227
17.2;10.2 An Informal Discussion;228
17.3;10.3 Formal Définitions of Programs;230
17.4;10.4 Logical Formulas Describing the Execution of a Program;233
17.5;10.5 Program Analysis by Resolution;234
17.6;10.6 The Termination and Response of Programs;239
17.7;10.7 The Set-of-Support Strategy and the Deduction of the Halting Clause;242
17.8;10.8 The Correctness and Equivalence of Programs;244
17.9;10.9 The Specialization of Programs;245
17.10;References;248
17.11;Exercises;249
18;Chapter 11. Deductive Question Answering, Problem Solving, and Program Synthesis;251
18.1;11.1 Introduction;251
18.2;11.2 Class A Questions;253
18.3;11.3 Class B Questions;254
18.4;11.4 Class C Questions;257
18.5;11.5 Class D Questions;260
18.6;11.6 Completeness of Resolution for Deriving Answers;267
18.7;11.7 The Principles of Program Synthesis;268
18.8;11.8 Primitive Resolution and Algorithm A
(A Program-Synthesizing Algorithm);275
18.9;11.9 The Correctness of Algorithm
A;284
18.10;11.10 The Application of Induction Axioms to Program Synthesis;288
18.11;11.11 Algorithm A (An Improved Program-Synthesizing Algorithm;292
18.12;References;296
18.13;Exercises;297
19;Chapter
12. Concluding Remarks;300
19.1;References;301
20;Appendix A;304
20.1;A.l A Computer Program Using Unit Binary Resolution;304
20.2;A.2 Brief Comments on the Program;307
20.3;A.3 A Listing of the Program;309
20.4;A.4 Illustrations;315
20.5;References;322
21;Appendix B;323
22;Bibliography;326
23;INDEX;342