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.