Return-Path: Date: Wed, 12 Jan 94 18:02:43 CST From: "Robert S. Boyer" To: nqthm-users@cli.com Subject: Nqthm-1992 Reply-To: boyer@cli.com 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