torkel@sics.se (Torkel Franzen) (06/09/90)
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.