🚀 go-pugleaf

torkel@sics.se (Torkel Franzen) writes:

>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
>  [...]

Could you please tell us what directory/filename(s) it can be found in on the
ftp site name you gave?  I looked about but could not seem to find anything
that looked interesting :-).  Also is the C version available somewhere there
too?

Rhys.

+===============================+==============================+
||  Rhys Weatherley             |  University of Queensland,  ||
||  rhys@batserver.cs.uq.oz.au  |  Australia.  G'day!!        ||
+===============================+==============================+