A Computational Logic

A Computational Logic

1st Edition - December 28, 1979

Write a review

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

Purchase options

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

Institutional Subscription

Free Global Shipping
No minimum order


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.

Table of Contents

  • Preface

    I. Introduction

    A. Motivation

    B. Our Formal Theory

    C. Proof Techniques

    D. Examples

    E. Our Mechanical Theorem-Prover

    F. Artificial Intelligence or Logic?

    G. Organization

    II. A Sketch of the Theory and Two Simple Examples

    A. An Informal Sketch of the Theory

    B. A Simple Inductive Proof

    C. A More Difficult Problem

    D. A More Difficult Proof

    E. Summary

    F. Notes

    III. A Precise Definition of the Theory

    A. Syntax

    B. The Theory of If and Equal

    C. Well-Founded Relations

    D. Induction

    E. Shells

    F. Natural Numbers

    G. Literal Atoms

    H. Ordered Pairs

    I. Definitions

    J. Lexicographic Relations

    K. Lessp and Count

    L. Conclusion

    IV. The Correctness of a Tautology-Checker

    A. Informal Development

    B. Formal Specification of the Problem

    C. The Former Definition of Tautology.Checker

    D. The Mechanical Proofs

    E. Summary

    F. Notes

    V. An Overview of How We Prove Theorems

    A. The Role of the User

    B. Clausal Representation of Conjectures

    C. The Organization of Our Heuristics

    D. The Organization of Our Presentation

    VI. Using Type Information to Simplify Formulas

    A. Type Sets

    B. Assuming Expressions True or False

    C. Computing Type Sets

    D. Type Prescriptions

    E. Summary

    F. Notes

    VII. Using Axioms and Lemmas as Rewrite Rules

    A. Directed Equalities

    B. Infinite Looping

    C. More General Rewrite Rules

    D. An Example of Using Rewrite Rules

    E. Infinite Backwards Chaining

    F. Free Variables in Hypotheses

    VIII. Using Definitions

    A. Nonrecursive Functions

    B. Computing Values

    C. Diving in to See

    IX. Rewriting Terms and Simplifying Clauses

    A. Rewriting Terms

    B. Simplifying Clauses

    C. The Reverse Example

    D. Simplification in the Reverse Example

    X. Eliminating Destructors

    A. Trading Bad Terms for Good Terms

    B. The Form of Elimination Lemmas

    C. The Precise Use of Elimination Lemmas

    D. A Nontrivial Example

    E. Multiple Destructors and Infinite Looping

    F. When Elimination Is Risky

    G. Destructor Elimination in the Reverse Example

    XI. Using Equalities

    A. Using and Throwing Away Equalities

    B. Cross-Fertilization

    C. A Simple Example of Cross-Fertilization

    D. The Precise Use of Equalities

    E. Cross-Fertilization in the Reverse Example

    XII. Generalization

    A. A Simple Generalization Heuristic

    B. Restricting Generalizations

    C. Examples of Generalizations

    D. The Precise Statement of the Generalization Heuristic

    E. Generalization in the Reverse Example

    XIII. Eliminating Irrelevance

    A. Two Simple Checks for Irrelevance

    B. The Reason for Eliminating Isolated Hypotheses

    C. Elimination of Irrelevance in the Reverse Example

    XIV. Induction and the Analysis of Recursive Definitions

    A. Satisfying the Principle of Definition

    B. Induction Schemes Suggested by Recursive Functions

    C. The Details of the Definition-Time Analysis

    D. Recursion in the Reverse Example

    XV. Formulating an Induction Scheme for a Conjecture

    A. Collecting the Induction Candidates

    B. The Heuristic Manipulation of Induction Schemes

    C. Examples of Induction

    D. The Entire Reverse Example

    XVI. Illustrations of Our Techniques via Elementary Number Theory

    A. Plus.Right.Id

    B. Commutativity2.of.Plus

    C. Commutativity.of.Plus

    D. Associativity.of.Plus

    E. Times

    F. Times.Zero

    G. Times.Add1

    H. Associativity.of.Times

    I. Difference

    J. Recursion.by.Difference

    K. Remainder

    L. Quotient

    M. Remainder.Quotient.Elim

    XVII. The Correctness of a Simple Optimizing Expression Compiler

    A. Informal Development

    B. Formal Specification of the Problem

    C. Formal Definition of the Compiler

    D. The Mechanical Proof of Correctness

    E. Notes

    XVIII. The Correctness of a Fast String Searching Algorithm

    A. Informal Development

    B. Formal Specification of the Problem

    C. Developing the Verification Conditions for the Algorithm

    D. The Mechanical Proofs of the Verification Conditions

    E. Notes

    XIX. The Unique Prime Factorization Theorem

    A. The Context

    B. Formal Development of the Unique Prime Factorization Theorem

    C. The Mechanical Proofs

    Appendix A. Definitions Accepted and Theorems Proved by Our System

    Appendix B. The Implementation of the Shell Principle

    Appendix C. Clauses for Our Theory



Product details

  • No. of pages: 414
  • Language: English
  • Copyright: © Academic Press 1979
  • Published: December 28, 1979
  • Imprint: Academic Press
  • eBook ISBN: 9781483277882

About the Authors

Robert S. Boyer

J Strother Moore

About the Editor

Thomas A. Standish

Ratings and Reviews

Write a review

There are currently no reviews for "A Computational Logic"