The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic

摘要

A well-known result of Ladner says that the satisfiability problem for K45, KD45, and S5 is NP-complete. This result implicitly assumes that there are infinitely many primitive propositions in the language; it is easy to see that the satisfiability problem for these logics becomes linear time if there are only finitely many primitive propositions in the language. By way of contrast, we show that the PSPACE-completeness results of Ladner and Halpern and Moses hold for the modal logics Kn, Tn, S4n, n ⩾ 1, and K45n, KD45n, S5n, n ⩾ 2, even if there is only one primitive proposition in the language. We go on to examine the effect on complexity of bounding the depth of nesting of modal operators. If we restrict to finite nesting, then the satisfiability problem is NP-complete for all the modal logics considered, but S4. If we then further restrict the language to having only finitely many primitive propositions, the complexity goes down to linear time in all cases.