boyer@CLI.COM (Robert S. Boyer) (04/19/88)
A Common Lisp version of our theorem-prover is now available under the
usual conditions: no license, no copyright, no fee, no support. The
system runs well in three Common Lisps: KCL, Symbolics, and Lucid.
There are no operating system or dialect conditionals, so the code may
well run in other implementations of Common Lisp.
Included as sample input is the work of Hunt on the FM8501
microprocessor and of Shankar on Goedel's incompleteness theorem and
the Church-Rosser theorem.
To get a copy follow these instructions:
1. ftp to Arpanet/Internet host cli.com.
(cli.com currently has Internet numbers
10.8.0.62 and 192.31.85.1)
2. log in as ftp, password guest
3. get the file /pub/nqthm/README
4. read the file README and follow the directions it gives.
Inquiries concerning tapes may be sent to:
Computational Logic, Inc., Suite 290
1717 W. 6th St.
Austin, Texas 78703
A comprehensive manual is available. For information on obtaining a
copy, write to the address above.
Bob Boyer J Moore
boyer@cli.com moore@cli.com
It seems possible that on May 1, 1988 all of Austin, Texas will be
disconnected from the Internet/Arpanet, for a while anyway. So
connections to cli.com may be very difficult starting May 1.