Efficient Local Reductions to Basic Modal Logic

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • Authors:
  • Fabio Papacchini
  • Cláudia Nalon
  • Ullrich Hustadt
  • Clare Dixon


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 satisability 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.

Bibliographical metadata

Original languageEnglish
Title of host publication28th International Conference on Automated Deduction
Publication statusAccepted/In press - 9 Apr 2021