🚀 go-pugleaf

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.