SAT-based proof search in intermediate propositional logics

We present a decision procedure for intermediate logics relying on a modular extension of the SAT-based prover intuitR for IPL (Intuitionistic Propositional Logic). Given an intermediate logic L and a formula α, the procedure outputs either a Kripke countermodel for α or the instances of the characteristic axioms of L that must be added to IPL in order to prove α. The procedure exploits an incremental SAT-solver; during the computation, new clauses are learned and added to the solver.