[comp.ai.digest] Boyer-Moore theorem prover in Common Lisp

K312631@AEARN.BITNET (Herwig Mayr) (03/20/88)

We are looking for a Common LISP version of the Boyer-Moore Theorem Prover
for use at our institute (mainly for lectures). Please, send replies over the
AIlist or to myself (K312631 at AEARN). Thank you||||

-herwig.

jbn@GLACIER.STANFORD.EDU (John B. Nagle) (03/21/88)

      Boyer and Moore use a Symbolics, but I ported it over to the version
of Franz Lisp that comes with 4.3BSD several years ago, and they merged the
code back into their system.  The changes were minor.  The system
used to be available by anonymous FTP from UTEXAS-20.ARPA, and still may be
on-line there.  Bob Boyer is now at Computational Logic, Inc. in Austin,
Texas.

					John Nagle