Return-Path: Date: Wed, 12 Jan 94 18:20:26 CST From: Matt Kaufmann To: nqthm-users@cli.com Subject: Pc-Nqthm-1992 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)