From: James Morales
Subject: I Need a Theorem Prover
Date: Mon, 21 Apr 1997 00:00:00 +0000
Message-ID: <5jh974$cnf$1@apakabar.cc.columbia.edu>

Does anyone have a theorem prover that I may be able to borrow? It needs to
be written in LISP. Thanks in advance.

From: Don Geddis
Subject: Re: I Need a Theorem Prover
Date: Tue, 22 Apr 1997 00:00:00 +0000
Message-ID: <slrn5lobso.rvf.geddis@meta.Tesserae.COM>

On Mon, 21 Apr 1997 22:51:57 -0400, James Morales <·····@columbia.edu> wrote:
> Does anyone have a theorem prover that I may be able to borrow? It needs to
> be written in LISP.

You should check out the FAQ lists for this newsgroup (comp.lang.lisp) as
well as for "comp.ai".  Both list many available theorem prover.

I wrote a low-quality inference engine for my thesis.  It happens to have the
two virtues of (1) being free, and (2) having the Lisp source code available.
You can find it at
	http://logic.stanford.edu/software/dtp/

But there are many more choices.

	-- Don
-- 
Don Geddis      ······@Tesserae.COM        http://geddis.stanford.edu/~geddis/
Sometimes you have to be careful when selecting a new nickname for yourself.
For instance, let's say you have chosen the nickname "Fly Head".  Normally, you
would think that "Fly Head" would mean a person who had beautiful swept-back
features, as if flying though the air.  But think again.  Couldn't it also mean
"having a head like a fly"?  I'm afraid some people might actually think that.
	-- Deep Thoughts, by Jack Handey