A New Approach to Clausification for Intuitionistic Propositional Logic

In recent years some papers have addressed the problem of the validity in Intuitionistic Propositional Logic and in some intermediate propositional logics using the approach proposed by Claessen and Rosén of reduction to Satisfiability Modulo Theories (SMT). This approach depends on an initial preprocessing phase that reduces the input formula in the intuitionistic language to an equivalent sequent in the language of clauses. In this work we present an extension of the clauses used by Claessen and Rosén that allows us to define a natural relationship between the semantics of the extended clauses and Kripke semantics. As an application, we show how Answer Set Programming can be used to check the intuitionistic validity of a formula and to generate Kripke countermodels for countersatisfiable formulas.