Computational Logic Handbook (eBook)

Formerly Notes and Reports in Computer Science and Applied Mathematics

Robert S. Boyer, J Strother Moore (Autoren)

Werner Rheinboldt, Daniel Siewiorek (Herausgeber)

eBook Download: PDF

2014 | 1. Auflage
426 Seiten
Elsevier Science (Verlag)
978-1-4832-7778-3 (ISBN)

Infos

Perspectives in Computing: A Computational Logic Handbook contains a precise description of the logic and a detailed reference guide to the associated mechanical theorem proving system, including a primer for the logic as a functional programming language, an introduction to proofs in the logic, and a primer for the mechanical theorem. The publication first offers information on a primer for the logic, formalization within the logic, and a precise description of the logic. Discussions focus on induction and recursion, quantification, explicit value terms, dealing with features and omissions, elementary mathematical relationships, Boolean operators, and conventional data structures. The text then takes a look at proving theorems in the logic, mechanized proofs in the logic, and an introduction to the system. The text examines the processes involved in using the theorem prover, four classes of rules generated from lemmas, and aborting or interrupting commands. Topics include executable counterparts, toggle, elimination of irrelevancy, heuristic use of equalities, representation of formulas, type sets, and the crucial check points in a proof attempt. The publication is a vital reference for researchers interested in computational logic.

Inhalt

Front Cover 1
A Computational Logic Handbook 4
Copyright Page 5
Table of Contents 6
Preface 12
Part I: 
18 
Chapter 1. Introduction 20
1.1. A Summary of the Logic and Theorem Prover 21
1.2. Some Interesting Applications 22
1.3. The Organization of this Handbook 26
Chapter 2. A Primer for the Logic 32
2.1. Syntax 33
2.2. Boolean Operators 34
2.3. Data Types 35
2.4. Extending the Syntax 43
2.5. Conventional Data Structures 45
2.6. Defining Functions 49
2.7. Recursive Functions on Conventional Data Structures 54
2.8. Ordinals 58
2.9. Useful Functions 60
2.10. The Interpreter 62
2.11. The General Purpose Quantifier 70
Chapter 3. Formalization Within the Logic 74
3.1. Elementary Programming Examples 77
3.2. Elementary Mathematical Relationships 82
3.3. Dealing with Omissions 85
3.4. Dealing with Features 93
3.5. Nondeterminism 103
3.6. Embedded Formal Systems 105
Chapter 4. A Precise Description of the Logic 110
4.1. Apologia 110
4.2. Outline of the Presentation 111
4.3. Formal Syntax 112
4.4. Embedded Propositional Calculus and Equality 118
4.5. The Shell Principle and the Primitive Data Types 122
4.6. Explicit Value Terms 128
4.7. The Extended Syntax—Abbreviations I 129
4.8. Ordinals 141
4.9. Useful Function Definitions 142
4.10. The Formal Metatheory 145
4.11. Quantification 153
4.12. SUBRPs and non-SUBRPs 155
4.13. Induction and Recursion 156
Chapter 5. Proving Theorems in the Logic 160
5.1. Propositional Calculus with Equality 161
5.2. Theorems about IF and Propositional Functions 164
5.3. Simple Theorems about NIL, CONS, and APPEND 166
5.4. The Associativity of APPEND 170
5.5. Simple Arithmetic 174
5.6. Structural Induction 179
Part II: Using the System 182
Chapter 6. Mechanized Proofs in the Logic 184
6.1. The Organization of Our Theorem Prover 184
6.2. An Example Proof—Associativity of TIMES 187
6.3. An Explanation of the Proof 190
Chapter 7. An Introduction to the System 194
7.1. The Data Base of Rules 194
7.2. Logical Events 196
7.3. A Summary of the Commands 197
7.4. Errors 199
7.5. Aborting a Command 199
7.6. Syntax and the User Interface 199
7.7. Confusing Lisp and the Logic 201
Chapter 8. A Sample Session with the Theorem Prover 204
Chapter 9. How to Use the Theorem Prover 224
9.1. REVERSE-REVERSE Revisited—Cooperatively 225
9.2. Using Lisp and a Text Editor as the Interface 230
9.3. The Crucial Check Points in a Proof Attempt 232
Chapter 10. How the Theorem Prover Works 236
10.1. The Representation of Formulas 237
10.2. Type Sets 238
10.3. Simplification 239
10.4. Elimination of Destructors 242
10.5. Heuristic Use of Equalities 243
10.6. Generalization 244
10.7. Elimination of Irrelevancy 245
10.8. Induction 245
Chapter 11. The Four Classes of Rules Generated from Lemmas 248
11.1. REWRITE 250
11.2. META 261
11.3. ELIM 264
11.4. GENERALIZE 265
Chapter 12. Reference Guide 268
12.1. Aborting or Interrupting Commands 268
12.2. ACCUMULATED-PERSISTENCE 270
12.3. ADD-AXIOM 271
12.4. ADD-SHELL 271
12.5. BOOT-STRAP 272
12.6. BREAK-LEMMA 274
12.7. BREAK-REWRITE 281
12.8. CH 283
12.9. CHRONOLOGY 285
12.10. COMPILE-UNCOMPILED-DEFNS 285
12.11. DATA-BASE 286
12.12. DCL 290
12.13. DEFN 291
12.14. DISABLE 293
12.15. DO-EVENTS 295
12.16. ELIM 296
12.17. ENABLE 297
12.18. Errors 297
12.19. Event Commands 299
12.20. EVENTS-SINCE 299
12.21. Executable Counterparts 299
12.22. Explicit Values 301
12.23. Extensions 302
12.24. FAILED-EVENTS 302
12.25. File Names 302
12.26. GENERALIZE 306
12.27. MAINTAIN-REWRITE-PATH 306
12.28. MAKE-LIB 307
12.29. META 307
12.30. Names—Events, Functions, and Variables 307
12.31. NOTE-LIB 308
12.32. NQTHM Mode 309
12.33. PPE 309
12.34. PROVE 309
12.35. PROVEALL 310
12.36. PROVE-LEMMA 311
12.37. R-LOOP 317
12.38. REDUCE-TERM-CLOCK 323
12.39. REWRITE 324
12.40. Root Names 324
12.41. Rule Classes 324
12.42. Time Triple 325
12.43. THM Mode 325
12.44. TOGGLE 325
12.45. TOGGLE-DEFINED-FUNCTIONS 326
12.46. TRANSLATE 326
12.47. UBT 327
12.48. UNBREAK-LEMMA 327
12.49. UNDO-BACK-THROUGH 328
12.50. UNDO-NAME 328
Chapter 13. Hints on Using the Theorem Prover 332
13.1. How to Write "Good" Definitions 332
13.2. How To Use REWRITE Rules 334
13.3. How to Use ELIM Rules 350
Chapter 14. Installation Guide 352
14.1. The Source Files 352
14.2. Compiling 353
14.3. Loading 355
14.4. Executable Images 356
14.5. Example Installation 357
14.6. Installation Problems 360
14.7. Shakedown 363
14.8. Packages 364
14.9. Example Event Files 365
Appendix I: 
368 
I.1. Some Preliminary Conventions 370
I.2. The Formal Definition of READ 372
I.3. The Formal Definition of TRANSLATE 382
I.4. EXSYN 398
Appendix II: The Primitive Shell Axioms 400
II.1. The Natural Numbers 401
II.2. The Ordered Pairs 403
II.3. The Literal Atoms 404
II.4. The Negative Integers 406
Appendix III: On the Difficulty of Proofs 408
References 414
Index 418
Perspectives in Computing 426

Produkt-Details

• Erscheint lt. Verlag: 10.5.2014
• Sprache: englisch
• Themenwelt: Mathematik / Informatik ► Mathematik
• Themenwelt: Technik
• ISBN-10: 1-4832-7778-X / 148327778X
• ISBN-13: 978-1-4832-7778-3 / 9781483277783