Nested Sequents for Intuitionistic Modal Logics via Structural Refinement
Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/Gutachten › Beitrag in Konferenzband › Beigetragen › Begutachtung
Beitragende
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
Originalsprache | Englisch |
---|---|
Titel | Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Proceedings |
Redakteure/-innen | Anupam Das, Sara Negri |
Erscheinungsort | Cham |
Herausgeber (Verlag) | Springer International Publishing AG |
Seiten | 409-427 |
Seitenumfang | 19 |
ISBN (elektronisch) | 978-3-030-86059-2 |
ISBN (Print) | 978-3-030-86058-5 |
Publikationsstatus | Veröffentlicht - 2021 |
Peer-Review-Status | Ja |
Externe IDs
Scopus | 85115260034 |
---|---|
ORCID | /0000-0003-3214-0828/work/142249492 |
Schlagworte
ASJC Scopus Sachgebiete
Schlagwörter
- Bi-relational model, Intuitionistic modal logic, Labelled sequent, Nested sequent, Proof theory, Propagation rule, Refinement