Nested Sequents for Intuitionistic Modal Logics via Structural Refinement

In Anupam Das & Sara Negri (eds.), Automated Reasoning with Analytic Tableaux and Related Methods: TABLEAUX 2021. pp. 409-427 (2021)
  Copy   BIBTEX

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. 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.

Links

PhilArchive

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
Gentzen sequent calculi for some intuitionistic modal logics.Zhe Lin & Minghui Ma - 2019 - Logic Journal of the IGPL 27 (4):596-623.
On some intuitionistic modal logics.Hiroakira Ono - 1977 - Bulletin of the Section of Logic 6 (4):182-184.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
Higher-order sequent-system for intuitionistic modal logic.Kosta Dosen - 1985 - Bulletin of the Section of Logic 14 (4):140-142.
On the unity of logic.Jean-Yves Girard - 1993 - Annals of Pure and Applied Logic 59 (3):201-217.
Metalogic of Intuitionistic Propositional Calculus.Alex Citkin - 2010 - Notre Dame Journal of Formal Logic 51 (4):485-502.
From Display to Labelled Proofs for Tense Logics.Agata Ciabattoni, Tim Lyon & Revantha Ramanayake - 2018 - In Anil Nerode & Sergei Artemov (eds.), Logical Foundations of Computer Science. Springer International Publishing. pp. 120 - 139.
Prefixed tableaus and nested sequents.Melvin Fitting - 2012 - Annals of Pure and Applied Logic 163 (3):291 - 313.

Analytics

Added to PP
2021-10-09

Downloads
223 (#91,508)

6 months
84 (#57,817)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Tim Lyon
Technische Universität Dresden

Citations of this work

Nested sequents for intermediate logics: the case of Gödel-Dummett logics.Tim S. Lyon - 2023 - Journal of Applied Non-Classical Logics 33 (2):121-164.

Add more citations

References found in this work

An introduction to modal logic: the Lemmon notes.E. J. Lemmon - 1977 - Oxford: Blackwell. Edited by Dana S. Scott.
Recursive unsolvability of a problem of thue.Emil L. Post - 1947 - Journal of Symbolic Logic 12 (1):1-11.
Deep Sequent Systems for Modal Logic.Kai Brünnler - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 107-120.

View all 9 references / Add more references