Deciding intuitionistic propositional logic via translation into classical logic

Abstract

We present a technique that efficiently translates prepositional intuitionistic formulas into propositional classical formulas. This technique allows the use of arbitrary classical theorem provers for deciding the intuitionistic validity of a given propositional formula. The translation is based on the constructive description of a finite counter-model for any intuitionistic non-theorem. This enables us to replace universal quantification over all accessible worlds by a conjunction over the constructed finite set of these worlds within the encoding of a refuting Kripke-frame. This way, no additional theory handling by the theorem prover is required.