[Zurück]

R. Kuznets, B. Lellmann:
"Grafting Hypersequents onto Nested Sequents";
Bericht für arXiv; Berichts-Nr. 1502.00814, 2015; 41 S.

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 𝖪𝟧 and 𝖪𝖣𝟧, as well as for extensions of the modal logics 𝖪 and 𝖪𝖣 with the axiom for shift reflexivity. The latter of these extensions is also known as 𝖲𝖣𝖫+ 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 𝖪𝟧 and 𝖪𝖣𝟧 yields simplified prefixed tableau calculi for these logic reminiscent of the simplified tableau system for 𝖲𝟧, which might be of independent interest.

http://arxiv.org/abs/1502.00814