boyer@CLI.COM (Robert S. Boyer) (04/23/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 Due to major changes in the Arpanet, getting through to cli.com may be difficult starting May 1 until one of the alternative Internet options is solidly in place.
atoenne@laura.UUCP (Andreas Toenne) (05/03/88)
In article <8804230021.AA05197@CLI.COM> boyer@CLI.COM (Robert S. Boyer) writes: >A Common Lisp version of our theorem-prover is now available under the >usual conditions: no license, no copyright, no fee, no support. The >To get a copy follow these instructions: > >1. ftp to Arpanet/Internet host cli.com. Ouch! Can anyone send me this theorem-prover by e-mail please? I have no ftp access :-( Please send it to the following BITNET Address, as UUCP (and Arpa) Mail costs me real $$. atoenne@ddoinf6.bitnet Thank you in advance Andreas Toenne