A Computational Logic Handbook

This book is a user's guide to a computational logic. A "computational logic"
is a mathematical logic that is both oriented towards discussion of computation
and mechanized so that proofs can be checked by computation. The
computational logic discussed in this handbook is that developed by Boyer and Moore.
This handbook contains a precise and complete description of our logic and a
detailed reference guide to the associated mechanical theorem proving system.
In addition, the handbook includes a primer for the logic as a functional
programming language, an introduction to proofs in the logic, a primer for the
mechanical theorem prover, stylistic advice on how to use the logic and theorem
prover effectively, and many examples.
The logic was last described completely in our book A Computational
Logic, [4], published in 1979. The main purpose of the book was to describe in
detail how the theorem prover worked, its organization, proof techniques,
heuristics, etc. One measure of the success of the book is that we know of three
independent successful efforts to construct the theorem prover from the book.