Correctness of an Incremental and Worst-Case Optimal Decision Procedure for Modal Logic with Eventualities

Mark Kaminski, Gert Smolka

We present a simple theory explaining the construction and the correctness of an incremental and worst-case optimal decision procedure for modal logic with eventualities. The proce…