"Local is Best: Efficient Reductions to Modal Logic K"

We present novel reductions of extensions of the basic modal logic K with axioms B, D, T, 4 and 5 to Separated Normal Form with Sets of Modal Levels SNFsml . The reductions typically result in smaller formulae than the reductions by Kracht. The reductions to SNFsml combined with a reduction to SNFml allow us to use the local reasoning of the prover KSP to determine the satisfiability of modal formulae in the considered logics. We show experimentally that the combination of our reductions with the prover KSP 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.