A Computational Logic Handbook: Second Edition
The second edition of the book A Computational Logic Handbook is now in
print.
Robert S. Boyer and J Strother Moore, A Computational Logic Handbook,
Second Edition, Academic Press, 1998, ISBN 0121229556. 518+xxv pages.
Be sure to mention "second edition".
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
- describes new syntax, including COND, CASE, LET, LIST*, and backquote
- describes some "higher order" inference procedures, including
"constrained functions" and "functional instantiation"
- documents more sophisticated control machinery for manipulating
very large theories
- introduces a "secure" proof-checking environment
- describes thousands of pages of fascinating example input dealing with
very difficult questions in formal methods and mathematics
- provides a formal parser for the syntax
- compares the proof complexity of many interesting checked examples
- includes much new tutorial help, especially for the many
new features
- contains a thorough bibliography of interesting Nqthm
applications
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.