Zeitschriftenartikel:
R. Kuznets, B. Lellmann:
"Grafting Hypersequents onto Nested Sequents";
Logic Journal of the IGPL,
24
(2016),
3;
S. 375
- 423.
Kurzfassung englisch:
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 K5 and KD5, as well as for extensions of the modal logics K and KD with the axiom for shift reflexivity. The latter of these extensions is also known as 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 K5 and KD5 yields simplified prefixed tableau calculi for these logic reminiscent of the simplified tableau system for S5, which might be of independent interest.
Schlagworte:
Hypersequents, nested sequents, tableaus, modal logic, decision procedures, complexity
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1093/jigpal/jzw005
Elektronische Version der Publikation:
http://doi.org/10.1093/jigpal/jzw005
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.