Nested Sequents for Intuitionistic Modal Logics via Structural Refinement

EasyChair Preprint 7080

Abstract

We employ a recently developed methodology---called "structural refinement"---to extract nested sequent systems for a sizable class of intuitionistic modal logics from their respective labelled sequent systems. Our nested systems incorporate propagation rules, parameterized with formal grammars, that encode certain frame conditions expressible as first-order Horn formulae and which correspond to a subclass of the Scott-Lemmon axioms. We show that our nested systems are sound, cut-free complete, and admit hp-admissibility of typical structural rules.

Keyphrases: Bi-relational model, Computer Science, Labelled sequent, Nested sequent, Propagation Graph, formal grammar, intuitionistic modal cube, intuitionistic modal logic, labelled formula, labelled system, labelled tree sequent, modal logic, nested sequent system, proof theory, propagation path, propagation rule, refinement, scott lemmon axiom, sequent system, structural refinement, tense logic, tree sequent

@booklet{EasyChair:7080,
  author    = {Tim Lyon},
  title     = {Nested Sequents for Intuitionistic Modal Logics via Structural Refinement},
  howpublished = {EasyChair Preprint 7080},
  year      = {EasyChair, 2021}}