Nested Sequents for Intuitionistic Modal Logics via Structural Refinement

Tim LyonTim Lyon

ISBN: 978-3-030-86058-5
Download
DOI Link

Tim Lyon
Nested Sequents for Intuitionistic Modal Logics via Structural Refinement
In Anupam Das, Sara Negri, eds., Automated Reasoning with Analytic Tableaux and Related Methods, 409-427, August 2021. Springer International Publishing

Details
Bibtex

KurzfassungAbstract
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.
Weitere Informationen unter:Further Information: Link
Projekt:Project: DeciGUT
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@inproceedings{L2021,
  author    = {Tim Lyon},
  title     = {Nested Sequents for Intuitionistic Modal Logics via Structural
               Refinement},
  editor    = {Anupam Das and Sara Negri},
  booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods},
  publisher = {Springer International Publishing},
  year      = {2021},
  month     = {August},
  pages     = {409-427},
  doi       = {10.1007/978-3-030-86059-2_24}
}