Path: utzoo!mnetor!uunet!lll-winken!lll-lcc!ames!pasteur!ucbvax!GLACIER.STANFORD.EDU!jbn
From: jbn@GLACIER.STANFORD.EDU (John B. Nagle)
Newsgroups: comp.ai.digest
Subject: Re: Boyer-Moore theorem prover in Common Lisp
Message-ID: <8803250644.AA22617@ucbvax.Berkeley.EDU>
Date: 20 Mar 88 16:57:29 GMT
Sender: daemon@ucbvax.BERKELEY.EDU
Organization: The Internet
Lines: 8
Approved: ailist@kl.sri.com


      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