Nested Sequents for Intuitionistic Modal Logics via Structural Refinement

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung


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. This method can be seen as a means by which labelled sequent systems can be transformed into nested sequent systems through the introduction of propagation rules and the elimination of structural rules, followed by a notational translation. The nested systems we obtain incorporate propagation rules that are parameterized with formal grammars, and which encode certain frame conditions expressible as first-order Horn formulae that 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.


TitelAutomated Reasoning with Analytic Tableaux and Related Methods
Redakteure/-innenAnupam Das, Sara Negri
Herausgeber (Verlag)Springer International Publishing AG
ISBN (elektronisch)978-3-030-86059-2
ISBN (Print)978-3-030-86058-5
PublikationsstatusVeröffentlicht - 2021

Externe IDs

Scopus 85115260034
ORCID /0000-0003-3214-0828/work/142249492