# Nested Sequents for Intuitionistic Modal Logics via Structural Refinement

arXiv: https://arxiv.org/abs/2107.01998 · HTML: https://mlsanity.com/paper/2107.01998/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Jul 2021.

## Built on by (most cited first, 2 of 2)

- [Automating Reasoning with Standpoint Logic via Nested Sequents](https://mlsanity.com/paper/2205.02749/) (2022)
- [Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents](https://mlsanity.com/paper/2404.15840/) (2024)

## Abstract (arXiv)

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.