A resolution theorem prover for intuitionistic logic

Abstract

We use the general scheme of building resolution calculi (also called the inverse method) originating from S.Maslov and G.Mints to design and implement a resolution theorem prover for intuitionistic logic. A number of search strategies are introduced and proved complete. The resolution method is shown to be a decision procedure for a new syntactically described decidable class of intuitionistic logic. The performance of our prover is compared with the performance of a tableau prover for intuitionistic logic presented in [12], using both the benchmarks from the latter and the theorems from J. von Plato-s constructive geometry [9].