Nested Sequents for Intuitionistic Modal Logics via Structural Refinement

From International Center for Computational Logic

Toggle side column

Nested Sequents for Intuitionistic Modal Logics via Structural Refinement

Tim LyonTim Lyon
Nested Sequents for Intuitionistic Modal Logics via Structural Refinement


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
  • 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}
}