@inproceedings{2906264917b7469da759d130d29a1504,
title = "Focused and synthetic nested sequents",
abstract = "Focusing is a general technique for transforming a sequent proof system into one with a syntactic separation of non-deterministic choices without sacrificing completeness. This not only improves proof search, but also has the representational benefit of distilling sequent proofs into synthetic normal forms. We show how to apply the focusing technique to nested sequent calculi, a generalization of ordinary sequent calculi to tree-like instead of list-like structures. We thus improve the reach of focusing to the most commonly studied modal logics, the logics of the modal S5 cube. Among our key contributions is a focused cutelimination theorem for focused nested sequents.",
author = "Kaustuv Chaudhuri and Sonia Marin and Lutz Stra{\ss}burger",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2016.; 19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016 ; Conference date: 02-04-2016 Through 08-04-2016",
year = "2016",
month = jan,
day = "1",
doi = "10.1007/978-3-662-49630-5\_23",
language = "English",
isbn = "9783662496299",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "390--407",
editor = "Christof L{\"o}ding and Bart Jacobs",
booktitle = "Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings",
}