How to obtain NQTHM

NOTE: Before you try to FTP this system make sure that:
  1. You understand the license agreement (see below).
  2. You understand the export limitations (see below).
  3. You have created a directory in which you wish to place it. The compressed image on NQTHM is almost four megabytes.
    4. .
To obtain the Unix version of Nqthm via FTP, first set `binary transfer mode' to `on'.
(My Mosaic viewer accomplishes this by setting the Load to local disk checkbox under the Options pulldown menu.)
Then, to FTP, click here: GET UNIX NQTHM.
You will get a compressed tar file, that is the file named "nqthm-1992.tar.Z" mentioned in the file README. Follow the instructions in this `README' file.

The rest of this page is initial portion of that `README' file. It resides in the directory /pub/nqthm/nqthm-1992/ on Internet host ftp.cli.com, where the publicly available version of Boyer and Moore's theorem-prover Nqthm, the 1992 version, may be found.

License Involved

Copying and use of Nqthm-1992 is authorized to those who have read and agreed with the terms in the Nqthm-1992 GENERAL PUBLIC SOFTWARE LICENSE, which may be found at the beginning of the Nqthm file `basis.lisp' and also in the files `nqthm-public-software-license.doc' and `nqthm-public-software-license.ps'.

Export Limitations

Under U. S. law, Nqthm-1992 may be legally exported from the U. S. to any country except as follows:
  1. No trade is permitted with either Iraq or Yugoslavia except under a special license, which would be very difficult to get.

  2. Electronic transfer (e.g., FTP) to any of North Korea, Cuba, Haiti or Libya is NOT permitted. Export on magnetic tape to these countries IS permitted.

This export policy complies with a legal opinion rendered by Computational Logic, Inc.'s attorneys in 1993.

Obtaining Nqthm-1992

One may obtain Nqthm-1992 by tape or ftp. We prefer that you obtain it by ftp, and there is no charge if you obtain it by ftp; we charge for tapes. If you are running on a Unix system the easiest means of obtaining Nqthm-1992 is to click on the highlighted GET UNIX NQTHM above.

Non-Unix FTP

To obtain Nqthm-1992 by ftp, connect to ftp.cli.com with the login name `anonymous' and your email address as the password. If you are not running a Unix or variant system, then ftp all of the files on the /pub/nqthm/nqthm-1992/ directory and its sub- and subsub-directories, except `nqthm-1992.tar.Z', and then go to the COMPILE instruction of this README file. Because there are over a hundred files and over a dozen subdirectories, making sure that you have gotten all of the files in this way can be tedious! So even if you are not running Unix, you may be well advised to try to get the files using some variant of the directions for UNIX FTP below. The next step is to read the README file.

Unix FTP

To obtain Nqthm-1992 by ftp, connect to ftp.cli.com with the login name `anonymous' and your email address as the password. If you are running a Unix or Unix variant, then `cd' to /pub/nqthm/nqthm-1992 and `get' the single file `nqthm-1992.tar.Z'. Be sure to use binary mode, e.g., execute the ftp command `binary' before doing the `get'. Checksum information for `nqthm-1992.tar.Z' may be found in the file `SUM', which you may obtain with another `get'; after you have obtained `nqthm-1992.tar.Z', executing `sum nqthm-1992.tar.Z' should produce the same results as are found in the file `SUM'. See the file `make.nqthm-1992.tar' for information on how `nqthm-1992.tar.Z' and `SUM' are created. `nqthm-1992.tar.Z' is almost four megabytes long. The next step is to read the README file.
This page is URL http://www.computationallogic.com/software/nqthm/obtaining.html