How to obtain NQTHM
NOTE: Before you try to FTP this system make sure that:
- You understand the license agreement (see below).
- You understand the export limitations (see below).
- You have created a directory in which you wish to place it.
The compressed image on NQTHM is almost four megabytes.
.
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:
- No trade is permitted with either Iraq or Yugoslavia except under a special
license, which would be very difficult to get.
- 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