rameshv@max.u.washington.edu (06/08/90)
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.
Thanks.
Ramesh.
P.S. Please address all replies to: joo@george.ee.washington.edu or
rameshv@george.ee.washington.edutorkel@sics.se (Torkel Franzen) (06/08/90)
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.
rhys@batserver.cs.uq.oz.au (Rhys Weatherley) (06/09/90)
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!! || +===============================+==============================+
torkel@sics.se (Torkel Franzen) (06/10/90)
In article <3885@moondance.cs.uq.oz.au> rhys@batserver.cs.uq.oz.au (Rhys Weatherley) writes: >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? I just checked our ftp/archive, which I understand is available to you when you ftp to sics.se. The Prolog version is there under the name sicstusft1.0.tar.Z, and the C version as ft1.2.Z. You should find a README file giving particulars about the files available for ftp, although there is an unfortunate discrepancy in regard to the C version, which is called 'ft1.1.tar.Z' in the README.