A Computational Logic Handbook

A Computational Logic Handbook

Formerly Notes and Reports in Computer Science and Applied Mathematics

1st Edition - October 28, 1988

Write a review

  • Authors: Robert S. Boyer, J Strother Moore
  • eBook ISBN: 9781483277783

Purchase options

Purchase options
DRM-free (PDF)
Sales tax will be calculated at check-out

Institutional Subscription

Free Global Shipping
No minimum order

Description

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.

Table of Contents


  • 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

Product details

  • No. of pages: 426
  • Language: English
  • Copyright: © Academic Press 1988
  • Published: October 28, 1988
  • Imprint: Academic Press
  • eBook ISBN: 9781483277783

About the Authors

Robert S. Boyer

J Strother Moore

About the Editors

Werner Rheinboldt

Daniel Siewiorek

Affiliations and Expertise

Carnegie-Mellon University

Ratings and Reviews

Write a review

There are currently no reviews for "A Computational Logic Handbook"