Skip to Main content Skip to Navigation

Focused and Synthetic Nested Sequents (Extended Technical Report)

Kaustuv Chaudhuri 1 Sonia Marin 1 Lutz Strassburger 1 
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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 cut-elimination theorem for focused nested sequents. This is an extended version of a paper with the same title and authors that appears in the Proceedings of the 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Eindhoven, Netherlands, 2-4 April 2016. This version contains full proofs of all the important lemmas and theorems.
Document type :
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download
Contributor : Kaustuv Chaudhuri Connect in order to contact the contributor
Submitted on : Monday, January 11, 2016 - 1:54:50 PM
Last modification on : Wednesday, February 2, 2022 - 3:55:20 PM
Long-term archiving on: : Tuesday, April 12, 2016 - 11:17:50 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution - NoDerivatives 4.0 International License


  • HAL Id : hal-01251722, version 2


Kaustuv Chaudhuri, Sonia Marin, Lutz Strassburger. Focused and Synthetic Nested Sequents (Extended Technical Report). [Research Report] Inria. 2016. ⟨hal-01251722v2⟩



Record views


Files downloads