Local is Best: Efficient Reductions to Modal Logic K

We present novel reductions of extensions of the basic modal logic with axioms , , , and to Separated Normal Form with Sets of Modal Levels _sml . The reductions typically result in smaller formulae than the reductions by Kracht. The reductions to _sml combined with a reduction to _ml allow us to use the local reasoning of the prover K_SP to determine the satisfiability of modal formulae in the considered logics. We show experimentally that the combination of our reductions with the prover K_SP performs well when compared with a specialised resolution calculus for these logics, the built-in reductions of the first-order prover SPASS, and the higher-order logic prover LEO-III.