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