We have shown how our framework provides a basis for new proof-theoretical method for establishing decidability and bounding the complexity of some non-classical logics, and, as examples, we have given PSPACE decision procedures for the propositional modal logics K, T, K4 and S4. We establish these bounds by combining restrictions on the structural rules of our labelled sequent systems with an analysis of the accessibility relation of the corresponding Kripke frames. Furthermore, we have shown that as a by-product of our analysis we can obtain justifications (and in some cases refinements) of the rules of standard sequent systems.
KeywordsModal Logic Decision Procedure Accessibility Relation Propositional Variable Relevance Logic
Unable to display preview. Download preview PDF.