An Intuitionistic Predicate Logic Theorem Prover

Sahlin, Dan and Franzén, Torkel and Haridi, Seif (1989) An Intuitionistic Predicate Logic Theorem Prover. [SICS Report]



A complete theorem prover for intuitionistic predicate logic based on the cut-free calculus is presented. It includes a treatment of "quasi-free" identity based on a delay mechanism and a special form of unification. Several important optimizations of the basic algorithm are introduced. The resulting system is available in source form from SICS; an Appendix gives some idea of its performance.

Item Type:SICS Report
Additional Information:Original report number R89001.
Uncontrolled Keywords:intuitionistic predicate logic, theorem proving
ID Code:2062
Deposited By:Vicki Carleson
Deposited On:28 Sep 2009
Last Modified:18 Nov 2009 15:59

Repository Staff Only: item control page