An intuitionistic predicate logic theorem prover

Abstract

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. © 1993 Oxford University Press.