Nested Sequents for Intuitionistic Modal Logics via Structural Refinement

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributedpeer-review

Contributors

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.

Details

Original languageEnglish
Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods
EditorsAnupam Das, Sara Negri
Place of PublicationCham
PublisherSpringer International Publishing AG
Pages409-427
Number of pages19
ISBN (electronic)978-3-030-86059-2
ISBN (print)978-3-030-86058-5
Publication statusPublished - 2021
Peer-reviewedYes

External IDs

Scopus 85115260034
ORCID /0000-0003-3214-0828/work/142249492