Hypersequent rules with restricted contexts for propositional modal logics

As part of a general research programme into the expressive power of different generalisations of the sequent framework we investigate hypersequent calculi given by rules of the newly introduced format of hypersequent rules with context restrictions. The introduced rule format is used to prove uniform syntactic cut elimination, decidability and complexity results. We also introduce transformations between hypersequent rules of this format and Hilbert axioms, entailing a result about the limits of such rules. As case studies, we apply our methods to several modal logics and obtain e.g. a complexity-optimal decision procedure for the logic S5 and new calculi for the logic K4.2 as well as combinations of modal logics in the form of simply dependent bimodal logics.