Path: utzoo!attcan!uunet!mailrus!tut.cis.ohio-state.edu!snorkelwacker!bloom-beacon!eru!luth!sunic!sics.se!sics.se!torkel
From: torkel@sics.se (Torkel Franzen)
Newsgroups: comp.lang.prolog
Subject: Re: Theorem Provers
Message-ID: <1990Jun8.082459.4371@sics.se>
Date: 8 Jun 90 08:24:59 GMT
References: <13882.266e78af@max.u.washington.edu>
Sender: news@sics.se
Organization: Swedish Institute of Computer Science, Kista
Lines: 20
In-Reply-To: rameshv@max.u.washington.edu's message of 7 Jun 90 22:54:23 GMT

In article <13882.266e78af@max.u.washington.edu> rameshv@max.u.washington.
edu writes:

   >I would like to know if there are any public domain first order predicate
   >logic theorem provers available.  I am interested in theorem provers which
   >can do constructive proofs.

   No doubt there are many such. In particular, all classical theorem provers
can do constructive proofs. What you really want, I hope, is a theorem
prover that can't do classical proofs, but only constructive ones. One
such, written in SICStus Prolog, is available from us by anonymous ftp
at sics.se, 192.16.123.90. As a theorem prover, it's pathetic. As an
intuitionistic theorem prover, it's pretty good. It's a joy to watch it
fail to prove e.g. Ex(p(x) -> Axp(x)), no matter how long you allow it to
go on. The algorithm is complete for intuitionistic validity. A decision
procedure for intuitionistic propositional logic is included.

  A version written in C is also available, and is very much more efficient.
The reason for this is that an essential optimization involving the storing
of old results couldn't be implemented in a worthwhile way in Prolog.