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 metalogical 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 prooftheoretic results thus avoiding duplicate work. We focus on modal logics characterized by frames with simple properties, i.e., properties that can be described by firstorder 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 nonlocality of systems of rules to at most two unlabelled sequent rules (2systems). The embedding yields new analytic calculi for the considered logics which can be used to formulate new natural deduction systems. Also, 2system derivations are made local.
