Download PDFOpen PDF in browser

Nested Sequents for Intuitionistic Modal Logics via Structural Refinement

EasyChair Preprint no. 7080

19 pagesDate: November 22, 2021


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, formal grammar, intuitionistic modal cube, intuitionistic modal logic, labelled formula, Labelled sequent, labelled system, labelled tree sequent, modal logic, Nested sequent, nested sequent system, proof theory, Propagation Graph, propagation path, propagation rule, refinement, scott lemmon axiom, sequent system, structural refinement, tense logic, tree sequent

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Tim Lyon},
  title = {Nested Sequents for Intuitionistic Modal Logics via Structural Refinement},
  howpublished = {EasyChair Preprint no. 7080},

  year = {EasyChair, 2021}}
Download PDFOpen PDF in browser