Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uwm.edu!rpi!zaphod.mps.ohio-state.edu!math.lsa.umich.edu!math.lsa.umich.edu!emv
From: torkel@sics.se (Torkel Franzen)
Newsgroups: comp.archives
Subject: [comp.lang.prolog] Re: Theorem Provers
Message-ID: <1990Jun8.205246.5488@math.lsa.umich.edu>
Date: 8 Jun 90 20:52:46 GMT
Sender: emv@math.lsa.umich.edu (Edward Vielmetti)
Reply-To: torkel@sics.se (Torkel Franzen)
Followup-To: comp.lang.prolog
Organization: University of Michigan, Department of Mathematics
Lines: 26
Approved: emv@math.lsa.umich.edu (Edward Vielmetti)
X-Original-Newsgroups: comp.lang.prolog

Archive-name: sics-theorem-prover/08-Jun-90
Original-posting-by: torkel@sics.se (Torkel Franzen)
Original-subject: Re: Theorem Provers
Archive-site: sics.se [192.16.123.90]
Reposted-by: emv@math.lsa.umich.edu (Edward Vielmetti)

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.