Handbook of Practical Logic and Automated Reasoning, by John Harrison, Cambridge University Press, 2009 ISBN 9780521899574

Abstract

The steady rise in interest in formal verification of software has naturally been accompanied by increased interest in the theory and tools of verification.While there are many textbooks of logic as well as user guides for the vast array of reasoning tools (automated and otherwise), much less is written about how to bridge the two, never mind good guides to the design problems of building reasoning tools.Harrison's Handbook of Practical Logic and Automated Reasoning explores that gap with flair.Even a casual glance at this hefty 700 page book will quickly dispel any "Handbook" impression which the title disingenuously gives: not a handbook at all, but rather a proper textbook.The style, far from that of a reference book, is deeply pedagogical, complete with a significant set of well-crafted exercises.It is well written using lucid prose, with the author taking great pains to elucidate important points, pausing to illustrate some subtleties, as well as being rather erudite in its coverage of the relevant literature, both historical and contemporary.As a textbook style introduction to the theory and practice of (first order, mathematical) logic and automated reasoning, it succeeds beautifully.This textbook masterfully weaves together theory and practice, by interleaving the development of the theoretical underpinnings of each topic covered with fairly well crafted code which implements the constructive portions of each chosen topic.In other words, this textbook is also a literate program, with all code written in OCaml, available from Harrison's web site.This really forces the author to cover many topics which are often, regrettably, omitted from other "practical" introductions to logic.Readers primarily interested in the theory covered by this book may find this aspect distracting, but I rather view this aspect of the book as one of its more endearing characteristics.The prose aspects of this literate textbook could easily serve as a model for years to come.The code is written using a fairly small subset of the Objective Caml language (no objects, Functors, higher rank polymorphism, nor polymorphic variants).While higher-order functions abound, the author nevertheless does not make heavy use of a more combinator-driven style which is more prevalent in the current functional literature.Eschewing Functors also means that the higher abstractions frequently seen in modern functional programs are also not used.While such a choice does broaden the audience which can easily understand the code, it would nevertheless be quite interesting to redevelop the same code, first in idiomatic Haskell, and then in Agda.But doing this would surely result in a research-level monograph, which was clearly not the author's intent.In other words, while this text does not use the most modern functional programming idioms, this was clearly an explicit decision, which makes sense in the context of the audience for this book.The set of topics covered might seem somewhat eclectic: propositional logic, first-order logic, equality reasoning, decidable problems, interactive theorem-proving and the limitations of all these approaches.In particular, "decidable problems" and "interactive theorem-proving" have traditionally been seen as belonging in different universes by the more "pure" adherents of formal reasoning.Of course, there have always been systems which eschewed this particular balkanisition, with ACL2, IMPS and PVS immediately coming to mind, and Harrison's own HOL Light following in the tradition.But this is now changing, as traditionally very pure