Nested Sequents for Intuitionistic Modal Logics via Structural Refinement

Speaker: Tim Lyon

Abstract: We employ a recently developed methodology---called "structural refinement"---to provide nested sequent systems for a sizable class of intuitionistic modal logics. The methodology consists of transforming labelled sequent systems into nested systems through the introduction of propagation rules and the elimination of structural rules, followed by a notational translation. Our propagation rules are parameterized with formal grammars that allow for certain frame conditions expressible as first-order Horn formulae and which correspond to a subclass of the Scott-Lemmon axioms to be encoded into our nested systems. The nested sequent systems we provide are sound, cut-free complete, and admit hp-admissibility of typical structural rules.