Announcement of a Newly Available Version of Pc-Nqthm

A new version of the "Pc-Nqthm" interactive enhancement of the Boyer-Moore
theorem proving program Nqthm is now available.  The new version is called
Pc-Nqthm-1992, and is an extension of the newly-released Nqthm-1992 version of
Nqthm.

As is the case with Nqthm-1992, this new version of Pc-Nqthm is almost
perfectly upwards compatible with the previous release.  Details may be found
in the file text/release-notes.txt that is provided with the system, but these
may in most cases be safely ignored.  Note however that like Nqthm-1992, all
Pc-Nqthm-1992 libraries (i.e., the .lib and .lisp files produced by MAKE-LIB)
are incompatible with those from the 1987 versions of Nqthm and Pc-Nqthm.

It is highly recommended that all Pc-Nqthm users obtain and install Nqthm-1992
and Pc-Nqthm-1992 and delete or archive away any earlier versions.  Note that
Pc-Nqthm-1992 is built on top of Nqthm-1992, and will not run on top of older
versions of Nqthm.

Included with the Nqthm-1992 distribution are a large number of
Pc-Nqthm-checked definitions and theorems formulated by Cowles, Goldschlag,
Kaufmann, Siebert, Verkest, Wilding, and Young.

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

To obtain Pc-Nqthm-1992, connect to Internet site ftp.cli.com by anonymous ftp,
`get' the file /pub/pc-nqthm/pc-nqthm-1992/README-pc, and follow the
instructions therein.

Source code for Pc-Nqthm-1992 is included in this distribution.  Building the
system requires only a few steps, given a running Common Lisp.  Pc-Nqthm-1992
is not dependent on any particular Common Lisp implementation or operating
system, in a variety of settings.  As a convenience for users of Unix-like
systems, there are `make' files for building and testing.  Also, a few
executable images are available.

Matt Kaufmann  (kaufmann@cli.com)