Article View: comp.ai
Article #8514Re: Need PD theorem prover
From: John - Nagle
Date: Fri, 22 Dec 1989 07:29
Date: Fri, 22 Dec 1989 07:29
11 lines
838 bytes
838 bytes
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
Technical Details
Message-ID:
<25268@cup.portal.com>Path:
arc1-ca.pugleaf.net!utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!snorkelwacker!apple!fox!portal!cup.portal.com!NagleReferences:
<639@uncle.UUCP>Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!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