Date: Wed, 12 Jan 94 18:17:38 CST
From: "Robert S. Boyer" <boyer@CLI.COM>
Message-Id: <9401130017.AA24136@dilbert.cli.com.CLI.COM>
To: Mark_Kantrowitz@GLINDA.OZ.CS.CMU.EDU
Subject: Nqthm
Reply-To: boyer@CLI.COM

We have just released a new version of the Boyer-Moore prover.  Last
July you asked about including something in a Prime Time Freeware book.
The following message tells you how to get what would be best,
just released.  Sorry if this is too late.

	      ANNOUNCEMENT OF A NEWLY AVAILABLE VERSION OF NQTHM


A new version of our theorem proving program Nqthm is now available.  The new
version is called Nqthm-1992.  The previous version was released in 1987.

The new version is almost perfectly upwards compatible with the previous
release.  Some minor bugs have been fixed, several new features have been
added, and a few performance enhancements have been made.  We know of no bug in
the previous release of Nqthm that can lead to a proof of (FALSE), but we
highly recommend to all Nqthm users that they obtain and install Nqthm-1992 and
delete or archive away any earlier version.

Included with the Nqthm-1992 distribution are thousands of Nqthm-checked
theorems formulated by Bevier, Boyer, Brock, Bronstein, Cowles, Flatau, Hunt,
Kaufmann, Kunen, Moore, Nagayama, Russinoff, Shankar, Talcott, Wilding, Yu, and
others.

There is a new license for Nqthm-1992 whose terms are more liberal than those
of the previous license.  In particular, no longer is reporting of who has
copies of Nqthm required of those who obtain or redistribute the new version.

The release of Nqthm-1992 includes three revised chapters of the book `A
Computational Logic Handbook', including Chapter 4, on the formal logic for
which the system is a prover, and Chapter 12, the reference guide to user
commands.  Change bars in the margin of the postscript version of these
chapters indicate what is new.

To obtain Nqthm-1992, connect to Internet site ftp.cli.com by anonymous ftp,
giving your email address as the password, `get' the file
/pub/nqthm/nqthm-1992/README, and follow the instructions therein.

Source code for Nqthm-1992 is included in this distribution.  Building the
system requires only a few steps, given a running Common Lisp.  Nqthm-1992 is
not dependent on any particular Common Lisp implementation or operating system.
It has been run under both CLTL1 and CLTL2 conforming implementations of Common
Lisp.  Nqthm-1992 has been run in a variety of settings, including under
Austin-Kyoto, CMU, Franz, Lucid, Macintosh, and Symbolics Common Lisps, and
under Linux, Macintosh, Sun, Symbolics, and Ultrix operating systems.  As a
convenience for users of Unix-like systems, there are `make' files for building
and testing.  Also, a few executable images are available, currently via AKCL
for both Sparcs and Linux-running PC-Clones and via MCL 2.0.1.

Robert S. Boyer  (boyer@cli.com)         J Strother Moore (moore@cli.com)

Computational Logic, Inc.
Austin, Texas

January, 1994