Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!snorkelwacker!apple!fox!portal!cup.portal.com!Nagle
From: Nagle@cup.portal.com (John - Nagle)
Newsgroups: comp.ai
Subject: Re: Need PD theorem prover
Message-ID: <25268@cup.portal.com>
Date: 22 Dec 89 07:29:53 GMT
References: <639@uncle.UUCP>
Organization: The Portal System (TM)
Lines: 11


     The Boyer-Moore theorem prover, as described in "A Computational
Logic" (Academic Press, 1979), is public domain, and copies can be
obtained from Boyer and Moore at the University of Texas.  But it is
a bit heavy going for casual use.  

     I once ported this beast to Franz Lisp, and a Common Lisp version
exists.  If anyone is seriously interested in working with it, I'd
be interested in talking to them.  But read the book first.

					John Nagle