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. 93413 Cham, Germany: pp. 409-427 (2021)
Download Edit this record How to cite View on PhilPapers
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.
PhilPapers/Archive ID
LYONSF
Upload history
Archival date: 2021-10-09
View other versions
Added to PP index
2021-10-09

Total views
16 ( #63,758 of 2,454,523 )

Recent downloads (6 months)
16 ( #37,207 of 2,454,523 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.