A Common Lisp version of an enhancement to the Boyer-Moore
theorem-prover that provides interactive capabilities and first-order
quantification is now available under the usual conditions:  no
license, no copyright, no fee, no support.  The system runs well in at
least three Common Lisps:  AKCL, Symbolics, and Lucid.  There are no
operating system or dialect conditionals, so the code may well run in
other implementations of Common Lisp.  However, it is important that
your Common Lisp supports redefinition of functions.  For example, KCL
(as opposed to AKCL) is not acceptable.

Before bothering to get a copy, first get a copy of the Boyer-Moore
theorem-prover.  Then, to get a copy of the interactive enhancement,
follow these instructions:

To get a copy follow these instructions:

1.   ftp to Internet host cli.com.
     (cli.com currently has Internet number
     192.31.85.1)
2.   log in as ftp, password guest
3.   get the file /pub/proof-checker/README-pc
4.   read the file README-pc 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 carefully written user's manual is available.  For information on
obtaining a copy, write to me at the address above.

Matt Kaufmann
kaufmann@cli.com