Computational logic is a fast-growing field. Written with graduate and
advanced undergraduate students in mind, this textbook introduces
computational logic from the foundations of first-order logic to
state-of-the-art decision procedures for arithmetic, data structures,
and combination theories. The textbook also presents a logical approach
to engineering correct software as an application of computational
logic. The increasing ubiquity of computers makes implementing correct
systems more important than ever. Verification exercises develop the
reader's facility in specifying and verifying software using logic. The
treatment of verification concludes with an introduction to the static
analysis of software, an important component of modern verification
systems. For readers interested in learning more about computational
logic, decision procedures, verification, and other areas of formal
methods, the final chapter outlines courses of further study.