An Intuitionistic Predicate Logic Theorem Prover
AN SAHLIN, Torkel Franzén, Seif Haridi · Journal of Logic and Computation · 1992
A complete theorem prover for intuitionistic predicate logic based on the cut-free sequent calculue is presented. It includes a treatment of ‘quasi-free’ identity based on a delay mechanism and a special form of unification. Several fairly far-reaching optimizations of the basic algorithm essential to its performance are introduced. The paper concludes with a set of benchmarks and execution data which may facilitate a comparison of algorithms for intuitionistic logic. The system is available in source code from SICS.