Nqthm, the Boyer-Moore prover



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

For installation instructions, see the file 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

  • Nqthm-checked theorems relating the SECD machine to the Lambda Calculus are presented in subdirectory trsecd.

  • 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 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.

    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.