Grafting hypersequents onto nested sequents

DOI10.1093/JIGPAL/JZW005zbMATH Open1405.03092arXiv1502.00814OpenAlexW1765007146MaRDI QIDQ4644546FDOQ4644546

Authors: Roman Kuznets, Björn Lellmann 

Publication date: 8 January 2019

Published in: Logic Journal of the IGPL (Search for Journal in Brave)

Abstract: We introduce a new Gentzen-style framework of grafted hypersequents that combines the formalism of nested sequents with that of hypersequents. To illustrate the potential of the framework, we present novel calculi for the modal logics $mathsfK5$ and $mathsfKD5$, as well as for extensions of the modal logics $mathsfK$ and $mathsfKD$ with the axiom for shift reflexivity. The latter of these extensions is also known as $mathsf{SDL}^{+}$ in the context of deontic logic. All our calculi enjoy syntactic cut elimination and can be used in backwards proof search procedures of optimal complexity. The tableaufication of the calculi for $mathsfK5$ and $mathsfKD5$ yields simplified prefixed tableau calculi for these logic reminiscent of the simplified tableau system for $mathsfS5$, which might be of independent interest.

Full work available at URL: https://arxiv.org/abs/1502.00814

Recommendations

• Labelled tree sequents, tree hypersequents and nested (deep) sequents
• Linear Nested Sequents, 2-Sequents and Hypersequents
• scientific article; zbMATH DE number 7668098
• Nested sequents for intuitionistic logics
• Focused and Synthetic Nested Sequents
• Nested sequents for intermediate logics: the case of Gödel-Dummett logics
• Nested sequent calculi for conditional logics
• scientific article; zbMATH DE number 6302922
• Hypersequents and Systems of Rules
• On nested sequents for constructive modal logics

zbMATH Keywords

complexitymodal logicdecision procedureshypersequentsnested sequentstableaus

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07)

Cited In (11)

• Through an inference rule, darkly
• Focused and Synthetic Nested Sequents
• Linear Nested Sequents, 2-Sequents and Hypersequents
• Rooted hypersequent calculus for modal logic \textsf{S5}
• Multicomponent proof-theoretic method for proving interpolation properties
• Compositional meaning in logic
• CUT ELIMINATION IN HYPERSEQUENT CALCULUS FOR SOME LOGICS OF LINEAR TIME
• Extensions of \textsf{K5}: proof theory and uniform Lyndon interpolation
• Some analytic systems of rules
• Grafted frames and S1 -completeness
• Title not available (Why is that?)

This page was built for publication: Grafting hypersequents onto nested sequents

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4644546)