Nested Sequents for Intuitionistic Modal Logics via Structural Refinement
arXiv:2107.01998 · doi:10.1007/978-3-030-86059-2_24
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.
References in corpus (5)
- On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics
- On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics
- Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics
- Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents
- Display to Labeled Proofs and Back Again for Tense Logics