@inproceedings{140c8f8a91774553b3dadb74f48e08b7,
title = "Labelled tree sequents, tree hypersequents and nested (Deep) sequents",
abstract = "We identify a subclass of labelled sequents called {"}labelled tree sequents{"} and show that these are notational variants of tree-hypersequents in the sense that a sequent of one type can be represented naturally as a sequent of the other type. This relationship can be extended to nested (deep) sequents using the relationship between tree-hypersequents and nested (deep) sequents, which we also show. We apply this result to transfer proof-theoretic results such as syntactic cut-admissibility between the tree-hypersequent calculus CSGL and the labelled sequent calculus G3GL for provability logic GL. This answers in full a question posed by Poggiolesi about the exact relationship between these calculi. Our results pave the way to obtain cut-free tree-hypersequent and nested (deep) sequent calculi for large classes of logics using the known calculi for labelled sequents, and also to obtain a large class of labelled sequent calculi for bi-intuitionistic tense logics from the known nested (deep) sequent calculi for these logics. Importing proof-theoretic results between notational variant systems in this manner alleviates the need for independent proofs in each system. Identifying which labelled systems can be rewritten as labelled tree sequent systems may provide a method for determining the expressive limits of the nested sequent formalism.",
keywords = "Cut-elimination, Labelled tree sequents, Notational variants, Proof theory",
author = "Rajeev Gor{\'e} and Revantha Ramanayake",
year = "2014",
language = "English",
series = "Advances in Modal Logic",
publisher = "College Publications",
pages = "279--299",
editor = "Torben Brauner and Lawrence Moss and Thomas Bolander and Silvio Ghilardi",
booktitle = "Advances in Modal Logic",
address = "United Kingdom",
note = "9th Conference on Advances in Modal Logic, AiML 2012 ; Conference date: 22-08-2012 Through 25-08-2012",
}