[comp.ai.digest] Availability of Boyer and Moore's Prover

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