Grafting hypersequents onto nested sequents

DOI10.1093/JIGPAL/JZW005MaRDI QIDQ4644546zbMATH OpenOpenAlexFDO

Authors Roman Kuznets, Björn Lellmann

Publication date 8 January 2019

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

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

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)

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.

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

Cited in

(11)

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

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)