Efficient SAT-based Proof Search in Intuitionistic Propositional Logic

We present an efficient proof search procedure for Intuitionistic Propositional Logic which involves the use of an incremental SATsolver. Basically, it is obtained by adding a restart operation to the system intuit by Claessen and Ros´en, thus we call our implementation intuitR. We gain some remarkable advantages: derivations have a simple structure; countermodels are in general small; using a standard benchmarks suite, we outperform intuit and other state-of-the-art provers.