How to obtain Pc-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 is several megabytes.

You will need to obtain Nqthm-1992 before installing Pc-Nqthm-1992. See obtaining the Unix version of Nqthm-1992.

To obtain the Unix version of Pc-Nqthm-1992 via FTP, first set `binary transfer mode' to `on'. My Mosaic viewer thinks this is done by the Load to local disk checkbox under the Options pulldown menu. Then, to FTP, click here: GET UNIX PC-NQTHM.
Follow the instructions in the README file.

The rest of this page is an initial portion of the `README' file (README-pc) for the directory /pub/pc-nqthm/pc-nqthm-1992/ on Internet host ftp://dirleton.csres.utexas.edu/pub, where a publicly available version of Kaufmann's `Pc-Nqthm' interactive enhancement of Boyer and Moore's theorem-prover Nqthm, the 1992 version, may be found. The string `pc' stands for `proof-checker,' and is used because this system is an interactive enhancement of Boyer and Moore's theorem prover. It contains other additional features as well, notably an implementation of first-order quantification.

License Involved

Copying and use of Pc-Nqthm-1992 is authorized to those who have read and agreed with the terms in the Pc-Nqthm-1992 GNU GENERAL PUBLIC LICENSE.

NOTE: The "misc/" subdirectory contains various Nqthm-1992 enhancements and tools, as described in the README file in that directory. Although these are all covered by the license agreement, they are not part of what we refer to as the `Pc-Nqthm-1992 system,' and in fact they may change at any time without notice.

Export Limitations

Under U. S. law, Pc-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 Pc-Nqthm-1992

IMPORTANT!! Pc-Nqthm-1992 is loaded on top of Boyer and Moore's `Nqthm-1992' theorem prover. You will need to obtain that system before installing Pc-Nqthm-1992. If you are running on a Unix system the easiest means of obtaining Nqthm-1992 is to click on the highlighted GET UNIX PC-NQTHM above.

Non-Unix FTP

To obtain Pc-Nqthm-1992 by ftp, connect to ftp://dirleton.csres.utexas.edu/pub 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/pc-nqthm/pc-nqthm-1992/ directory and its sub- and subsub-directories, except `pc-nqthm-1992.tar.Z', and then go to the COMPILE instruction of this file README-pc. Because there are a large number of files and 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-pc file.

Unix FTP

To obtain Pc-Nqthm-1992 by ftp, connect to ftp://dirleton.csres.utexas.edu/pub 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/pc-nqthm/pc-nqthm-1992 and `get' the single file `pc-nqthm-1992.tar.Z'. Be sure to use binary mode, e.g., execute the ftp command `binary' before doing the `get'. Checksum information for `pc-nqthm-1992.tar.Z' may be found in the file `SUM', which you may obtain with another `get'; after you have obtained `pc-nqthm-1992.tar.Z', executing `sum pc-nqthm-1992.tar.Z' should produce the same results as are found in the file `SUM'. See the file `make.pc-nqthm-1992.tar' for information on how `pc-nqthm-1992.tar.Z' and `SUM' are created. `pc-nqthm-1992.tar.Z' is several megabytes long.