Sciweavers

Share
FOSSACS
2016
Springer

Focused and Synthetic Nested Sequents

3 years 6 months ago
Focused and Synthetic Nested Sequents
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.
Kaustuv Chaudhuri, Sonia Marin, Lutz Straßbu
Added 03 Apr 2016
Updated 03 Apr 2016
Type Journal
Year 2016
Where FOSSACS
Authors Kaustuv Chaudhuri, Sonia Marin, Lutz Straßburger
Comments (0)
books