skr@uncle.UUCP (Steve K. Roggenkamp) (12/18/89)
I'm looking for a public domain theorem prover, preferably written in C or Xlisp. I do not have ftp access to Internet, but I can uucp or email. Thanks for any assistance. If there is enough interest, I'll summarize to the net. Steve -- Steven K. Roggenkamp, skr@uncle.UUCP, n8emr!uncle!skr@osu-cis.cis.ohio-state.edu (614) h:792-8236, w:764-4208;
Nagle@cup.portal.com (John - Nagle) (12/22/89)
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