Pavlovi, S. (2018). Proof theory for modal logics : embedding between hypersequent calculi and systems of rules [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2018.58584
Modal logics extend classical logic with modal operators that enable us to finely qualify the truth of a proposition. Due to their expressiveness and flexibility, they are used in many areas of computer science. Logical calculi are useful tools for investigating computational and meta-logical properties of logics; moreover, when analytic, they are the base to develop automated reasoning tools. In recent years, a plethora of new formalisms has been introduced, yielding proof systems for many logics. The formalisms may vary in their expressive powers, could be more suitable for certain applications, or may reveal different properties of the logic at hand. With a large number of formalisms comes the need to investigate the relationships between them. In particular, it is important to relate their expressive powers, which can be done through embeddings procedures that given a calculus in one formalism produce a calculus for the same logic in another formalism. Embeddings also allow the transfer of some proof-theoretic results thus avoiding duplicate work. We focus on modal logics characterized by frames with simple properties, i.e., properties that can be described by first-order formulae of a restricted form. The starting point of our investigation are analytic hypersequent calculi for these logics, a generalization of sequent calculi operating on finite multisets of sequents. Extending the methods of Ciabattoni and Genco, we provide an embedding between these calculi and sequent calculi extended by systems of rules sets of sequent rules sharing schematic variables that can only be applied in a predetermined order. We restrict the vertical non-locality of systems of rules to at most two unlabelled sequent rules (2-systems). The embedding yields new analytic calculi for the considered logics which can be used to formulate new natural deduction systems. Also, 2-system derivations are made local.