HOW TO OBTAIN NQTHM, THE BOYER-MOORE PROVER

All the Lisp sources, much documentation, and many examples for Nqthm-1992,
the Boyer-Moore prover, may be found at ftp.cs.utexas.edu in the directory
/pub/boyer/nqthm/. To get everything, fetch the file



      nqthm-2nd-edition.tar.gz

For installation instructions, see the file



      nqthm-1992/README

which may also found on the nqthm-2nd-edition.tar.gz file.

The directory /pub/boyer/nqthm/nqthm-1992-images of ftp.cs.utexas.edu
contains various ready-to-run executable images for Nqthm under GCL/Sparc,
GCL/Linux, and MCL/Mac.

The directory /pub/boyer/nqthm/nqthm-1992 of ftp.cs.utexas.edu contains, in
uncompressed and untarred form all of the directories and files, all of the
sources, examples, and distributed documentation for the entirety of
Nqthm-1992. To put it another way, that directory holds the contents of
nqthm-2nd-edition.tar.gz. The total is about 24 megabytes, several hundred
files. Generally, it is more efficient to obtain these files via the
aforementioned nqthm-2nd-edition.tar.gz. However, there may be some people
for whom .gz (gunzip) and .tar (Unix file grouping technique) are not
options.

NQTHM-USERS EMAIL LIST

There is a mailing list for discussion of Nqthm,
nqthm-users@cs.utexas.edu. To join, send an email message to
nqthm-users-request@cs.utexas.edu. The archive of this mailing group may be
found at ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/nqthm-users-mail-archive.

NQTHM-RELATED NEWS
o Nqthm-checked theorems relating the SECD machine to the Lambda Calculus
are presented in subdirectory trsecd.
o A second edition of A Computational Logic Handbook has been published by
Academic Press. ISBN 0-12-122955-6.

NQTHM BIBLIOGRAPHY

A bibliography of Nqthm-related publications may be found at
ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/nqthm-bibliography.html.

NQTHM-RELATED PROBLEMS?

Report problems with Nqthm to
    o Bob Boyer, boyer at cs.utexas.edu, http://www.cs.utexas.edu/users/boyer/
    o J Moore, moore at cs.utexas.edu, http://www.cs.utexas.edu/users/moore/

Bugs

See the file ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/bugs.text for
information on fixing bugs in Nqthm-1992.

NQTHM WORKAROUNDS

OpenMCL

See the file ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/openmcl-notes.text
for information on building and running Nqthm-1992 under OpenMCL.

Allegro Common Lisp/ACL

It appears that the spec for DUMPLISP in Allegro has changed between 1992 and
2002.

 See the file ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/allegro-work-around.text

To speed things up a bit it may be a good idea to change NQTHM-READTABLE as
mentioned for OpenMCL.


Clisp

See the file ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/clisp-notes.text for
information on building and running Nqthm-1992 under Clisp.

CMUCL

See the file ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/cmulisp-notes.text for
information on building and running Nqthm-1992 under CMUCL.

RELATED LINKS

Here are two links we recommend to the literature on formal methods and
automated reasoning.
    o Jonathan Bowen's Formal Methods Page
      http://www.comlab.ox.ac.uk/archive/formal-methods.html
    o Michael Kohlhase and Carolyn Talcott's Automated Reasoning Page
      http://www-formal.stanford.edu/clt/ARS/ars-db.html

For information about a prover to which Nqthm was a precursor, see the Acl2
Web Page http://www.cs.utexas.edu/users/moore/acl2/acl2-doc.html.