A Recipe for the Complexity Analysis of Non-Classical Logics

In previous work, we introduced a framework for the uniform formalization of families of non-classical logics with Kripke semantics, such as modal and relevance logics. Here we show how to use this framework to analyze the complexity of the decision problem for these logics, also in a uniform way. The result is a recipe: the user contributes bounds on structural reasoning and the accessibility relation associated with the Kripke semantics and the result is a decision procedure with bounded space requirements. As examples, we give PSPACE decision procedures for the modal logics K4 and S4, and for a positive fragment of the relevance logic B.