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
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.
See the file ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/bugs.text for information on fixing bugs in Nqthm-1992.
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
To speed things up a bit it may be a good idea to change NQTHM-READTABLE as mentioned for OpenMCL.
See the file ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/clisp-notes.text for information on building and running Nqthm-1992 under Clisp.
See the file ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/cmulisp-notes.text for information on building and running Nqthm-1992 under CMUCL.
Here are two links we recommend to the literature on formal methods and automated reasoning.
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.