Efficient Local Reductions To Basic Modal Logic

We present novel reductions of the propositional modal logics KB, KD, KT, K4 and K5 to Separated Normal Form with Sets of Modal Levels. The reductions result in smaller formulae than the well-known reductions by Kracht and allow us to use the local reasoning of the prover KSP to determine the satisfiability of modal formulae in these 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 and with the built-in reductions of the first-order prover SPASS.