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
Part I. The Logic
1. Introduction
1.1. A Summary of the Logic and Theorem Prover
1.2. Some Interesting Applications
1.3. The Organization of this Handbook
2. A Primer for the Logic
2.1. Syntax
2.2. Boolean Operators
2.3. Data Types
2.4. Extending the Syntax
2.5. Conventional Data Structures
2.6. Defining Functions
2.7. Recursive Functions on Conventional Data Structures
2.8. Ordinals
2.9. Useful Functions
2.10. The Interpreter
2.11. The General Purpose Quantifier
3. Formalization Within the Logic
3.1. Elementary Programming Examples
3.2. Elementary Mathematical Relationships
3.3. Dealing with Omissions
3.4. Dealing with Features
3.5. Nondeterminism
3.6. Embedded Formal Systems
4. A Precise Description of the Logic
4.1. Apologia
4.2. Outline of the Presentation
4.3. Formal Syntax
4.4. Embedded Propositional Calculus and Equality
4.5. The Shell Principle and the Primitive Data Types
4.6. Explicit Value Terms
4.7. The Extended Syntax-Abbreviations I
4.8. Ordinals
4.9. Useful Function Definitions
4.10. The Formal Metatheory
4.11. Quantification
4.12. Subrps and Non-Subrps
4.13. Induction and Recursion
5. Proving Theorems in the Logic
5.1. Propositional Calculus with Equality
5.2. Theorems about If and Propositional Functions
5.3. Simple Theorems about Nil, Cons, and Append
5.4. The Associativity of Append
5.5. Simple Arithmetic
5.6. Structural Induction
Part II. Using the System
6. Mechanized Proofs in the Logic
6.1. The Organization of Our Theorem Prover
6.2. An Example Proof-Associativity of Times
6.3. An Explanation of the Proof
7. An Introduction to the System
7.1. The Data Base of Rules
7.2. Logical Events
7.3. A Summary of the Commands
7.4. Errors
7.5. Aborting a Command
7.6. Syntax and the User Interface
7.7. Confusing Lisp and the Logic
8. A Sample Session with the Theorem Prover
9. How to Use the Theorem Prover
9.1. Reverse-Reverse Revisited-Cooperatively
9.2. Using Lisp and a Text Editor as the Interface
9.3. The Crucial Check Points in a Proof Attempt
10. How the Theorem Prover Works
10.1. The Representation of Formulas
10.2. Type Sets
10.3. Simplification
10.4. Elimination of Destructors
10.5. Heuristic Use of Equalities
10.6. Generalization
10.7. Elimination of Irrelevancy
10.8. Induction
11. The Four Classes of Rules Generated from Lemmas
11.1. Rewrite
11.2. Meta
11.3. Elim
11.4. Generalize
12. Reference Guide
12.1. Aborting or Interrupting Commands
12.2. Accumulated-Persistence
12.3. Add-Axiom
12.4. Add-Shell
12.5. Boot-Strap
12.6. Break-Lemma
12.7. Break-Rewrite
12.8. Ch
12.9. Chronology
12.10. Compile-Uncompiled-Defns
12.11. Data-Base
12.12. Dcl
12.13. Defn
12.14. Disable
12.15. Do-Events
12.16. Elim
12.17. Enable
12.18. Errors
12.19. Event Commands
12.20. Events-Since
12.21. Executable Counterparts
12.22. Explicit Values
12.23. Extensions
12.24. Failed-Events
12.25. File Names
12.26. Generalize
12.27. Maintain-Rewrite-Path
12.28. Make-Lib
12.29. Meta
12.30. Names-Events, Functions, and Variables
12.31. Note-Lib
12.32. Nqthm Mode
12.33. Ppe
12.34. Prove
12.35. Proveall
12.36. Prove-Lemma
12.37. R-Loop
12.38. Reduce-Term-Clock
12.39. Rewrite
12.40. Root Names
12.41. Rule Classes
12.42. Time Triple
12.43. Thm Mode
12.44. Toggle
12.45. Toggle-Defined-Functions
12.46. Translate
12.47. Ubt
12.48. Unbreak-Lemma
12.49. Undo-Back-Through
12.50. Undo-Name
13. Hints on Using the Theorem Prover
13.1. How to Write "Good" Definitions
13.2. How To Use Rewrite Rules
13.3. How to Use Elim Rules
14. Installation Guide
14.1. The Source Files
14.2. Compiling
14.3. Loading
14.4. Executable Images
14.5. Example Installation
14.6. Installation Problems
14.7. Shakedown
14.8. Packages
14.9. Example Event Files
Appendix I. A Parser for the Syntax
I.1. Some Preliminary Conventions
I.2. The Formal Definition of Read
I.3. The Formal Definition of Translate
I.4. Exsyn
Appendix II. The Primitive Shell Axioms
II.1. The Natural Numbers
II.2. The Ordered Pairs
II.3. The Literal Atoms
II.4. The Negative Integers
Appendix III. On the Difficulty of Proofs
References
Index