A Computational Logic

Front Cover
Robert S. Boyer, J Strother Moore
Academic Press, Jan 1, 1979 - MATHEMATICS - 397 pages
0 Reviews
A sketch of the theory and two simple examples; A precise definition of the theory; The correctness of a tautology-checker; An overview of how we prove theorems; Using type information to simplify formulas; Using axioms and lemmas as rewrite rules; Using definitions; Rewriting terms and simplifying clauses; Eliminating destructors; Using equalities; Generalization; Eliminating irrelevance; Induction and the analysis of recursive definitions; Formulating an induction scheme for a conjecture; Illustrations of our techniques via elementary number theory; The correctness of a simple optimizing expression compiler; The correctness of a fast string searching algorithm; The unique prime factorization theorem.

From inside the book

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

A Sketch of the Theory and Two Simple Examples
8
A Precise Definition of the Theory
28
The Correctness of a TautologyChecker
56
Copyright

17 other sections not shown

Other editions - View all

Common terms and phrases

References to this book

All Book Search results »

Bibliographic information