A Computational Logic Handbook: Second Edition

The second edition of the book A Computational Logic Handbook is now in print.

The second edition is the authoritative documentation for Nqthm-1992, the most recent edition of the Boyer-Moore prover, which may be obtained with sources and without fee at

In addition to a very large number of minor corrections and improvements to the first edition, here are some of the major differences of the second edition over the first P. S. There is a "new" release of Nqthm-1992 available at ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/index.html. However, this is actually only a "bureaucratic" update to make slightly easier the life of folks who wish to install Nqthm from scratch. This new release combines the Nqthm-1992 "release" of 1994 with the "examples" of 1995. In other words, if you already have a working Nqthm-1992 and the 1995 examples release, it's probably a waste of your time to do a reinstallation. (There is actually something new included: the ancient and crufty but operational Lisp code for our Fortran Verification Condition Generator, in directory examples/fortran-vcg.)

Main page.