\documentclass[smallcondensed]{svjour3}
\usepackage{url}

\journalname{Journal of Automated Reasoning}
\begin{document}

\title{``Handbook of Practical Logic and Automated Reasoning,''
by John R. Harrison,
Cambridge University Press, 2009}
\titlerunning{``Handbook of Practical Logic and Automated
Reasoning''}
\author{Freek Wiedijk}
\institute{Freek Wiedijk \\
Institute for Computing and Information Sciences,
Radboud University Nijmegen \\
%Heyendaalseweg 135, 6525 AJ Nijmegen, The Netherlands \\
\email{freek@cs.ru.nl}}
\date{}
\maketitle

\noindent
John Harrison's \emph{Handbook of Practical Logic and Automated
Reasoning} strongly reminds me of
Donald Knuth's \emph{The Art of Computer Programming}.
Both clearly are masterpieces.
And both scare me.
They are so comprehensive, so erudite,
and the information density is so high, that
one really
has to pay attention to get the most from the exposition.
Also, both are a bit idiosyncratic.
On the other hand, reading those books is an utter pleasure,
because everything is so beautifully presented and there
is so much to learn.

The \emph{Handbook of Practical Logic and Automated Reasoning}
then, is about automation in mathematical logic.
Theorem
proving with a computer only becomes practical when mundane
proof tasks are performed automatically (the two main
types of automation being `decision procedures' and `proof
search').
The best interactive theorem provers are those in
which this kind of automation has been developed furthest.
The \emph{Handbook} is a comprehensive treatment of this
kind of automation.
%John Harrison is one of the world experts in this area,
%and he now has written \emph{the} handbook on this subject.

The book consists of three strains that have been woven
together expertly.
The first strain consists of English
prose, treating the topics of the book in computer
science style.
The second strain is a mathematical
treatment consisting of definitions and theorems with full
mathematical proofs.
And the third strain is the source
code of a computer program in the programming language
OCaml, that implements \emph{everything} that is being treated
in detailed working code.

When reading the book one can ignore the second and third
strains without losing understanding of the subject.
If one thinks `Yes, I believe that that theorem holds, I
am not interested in the details of the proof right now',
one can skip over the proof without getting lost.
Or if
one thinks, `Yes, I roughly understand how that works, I
believe that it can be implemented', one can skip over
the program source without problems too.
However, \emph{if}
one is interested in the details of either the mathematics
or the implementation, it is all there.

If one strips the English from the book, one gets the
\emph{full} source of a beautiful self-contained theorem prover.
The book even includes the source for mundane things
like parsing and pretty-printing.
It shows the power
of functional programming that it is possible to give
full implementations of so many algorithms in a book of
681 pages, which still also treats everything in a way
that is understandable without looking at the code.
It also shows how cleverly John Harrison has built a
`theorem proving workbench' in which various pieces are
reused over and over again.
In some sense the book is
`just' an annotated listing of a program.
This probably
will turn some readers off, but as already said, even when
skipping over the code one still has a very readable and
detailed handbook.

The code from the book can be downloaded from
\begin{center}
\url{http://www.cl.cam.ac.uk/~jrh13/atp/}
\end{center}
and loaded into an
interactive OCaml session.
That way, one can easily experiment
with everything that the book discusses while reading it.

It should be noted that the theorem prover from the book
is \emph{not} John Harrison's industrial strength theorem
prover HOL Light.
The prover from the book implements
first order logic, while HOL Light is higher order.
In fact the book only briefly mentions higher order logic
on page 122.
Almost all interesting proof
automation apparently can be presented in the domain of
first order logic.
Another difference between these two theorem
provers is that unlike HOL Light the program from the book
is purely functional.
A nice challenge for the Haskell
community might be to create an attractive Haskell version.

The book seems to also be intended as a textbook of
mathematical logic, as it introduces propositional logic
and first order predicate logic from scratch.
Still, it
mostly treats highly technical subjects that will only
be digestible to people who already are well-versed in
mathematical logic.
Still, the book \emph{is} self-contained
and a smart novice {could} in theory understand everything
by paying close attention.

The table of contents of the \emph{Handbook} is deceptively
simple:
\begin{enumerate}
\item Introduction
\item Propositional logic
\item First-order logic
\item Equality
\item Decidable problems
\item Interactive theorem proving
\item Limitations
\end{enumerate}
\noindent
Hidden within these chapters is a wide range of subjects.
For example Chapter 4 contains a comprehensive overview
of term rewriting (including termination orderings and
Knuth-Bendix completion).
Chapter 5 treats among many
other subjects Buchberger's algorithm for the calculation of
Groebner bases (including applications like geometric theorem
proving).
Chapter 7 contains a very nice presentation
of Goedel's first incompleteness theorem (including lots
of code for experimenting with the machinery used in the
proof).
Note that proofs like the one of Goedel's theorem
are not just sketched.
Everything is developed and proved
in full detail.

The presentation of logic in the book is sometimes a
bit idiosyncratic.
Occasionally a path into a subject is
taken that does not follow the most `standard' treatment.
The choice of presentation then seems to have been influenced
by what fits nicely in the OCaml implementation.

As an example take the treatment of first order predicate
logic.
The semantics of first order logic is given
in Chapter 3, but a proof system only is presented in
Chapter 6, and then only as a Hilbert-style calculus.
Natural deduction and sequent calculus are sketched in a few pages, but
maybe too briefly for a person who does not know these systems already.
Also following Gentzen the notation $\Gamma \rightarrow p$ is used for what now is usually
written as $\Gamma \vdash p$.
After defining the Hilbert-style calculus, a beautiful LCF-style
implementation of this proof system is developed, and the
completeness theorem for first order logic is proved from
the fact that that implementation can execute a complete
proof search procedure.
Clearly, the theory of first order logic
(semantics, proof system, completeness) is all there,
but it is not put in one place.
Like many of the subjects it is woven throughout the book.

As the semantics are treated before the proof system, most
of the theory is developed in terms of the semantics.
This seems one of the themes of the book.

The book refers often to the historical background of
the various subjects, and the Further Reading sections
contain many pointers into the literature, referring to an
impressive list of references that goes on for 37 pages.
Each chapter also is accompanied by many interesting and
sometimes very challenging Exercises.

John Harrison is one of the foremost researchers in the
field of interactive theorem proving.
His HOL Light is
one of the best theorem provers in existence,
and his work
on formalization of mathematics is at the forefront of
the technology.
%And his daytime job at Intel is to prove
%algorithms running on actual hardware chips correct.
Now he has written what clearly will be \emph{the} book about
automation in theorem proving.

People often ask me whether they should buy this book.
My answer then always is: yes, \emph{of course} you should buy
this book.
It is a masterpiece.
But beware!
It might also scare you.

\end{document}