Focused and Synthetic Nested Sequents

Kaustuv Chaudhuri 1 Sonia Marin 1 Lutz Straßburger 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Communication dans un congrès
Bart Jacobs; Christof Löding. FOSSACS 2016 - 19th International Conference Foundations of Software Science and Computation Structures, Apr 2016, Eindhoven, Netherlands. Springer, 9634, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-662-49630-5_23〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01417618
Contributeur : Lutz Straßburger <>
Soumis le : jeudi 15 décembre 2016 - 17:19:12
Dernière modification le : jeudi 10 mai 2018 - 02:06:42

Identifiants

Citation

Kaustuv Chaudhuri, Sonia Marin, Lutz Straßburger. Focused and Synthetic Nested Sequents. Bart Jacobs; Christof Löding. FOSSACS 2016 - 19th International Conference Foundations of Software Science and Computation Structures, Apr 2016, Eindhoven, Netherlands. Springer, 9634, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-662-49630-5_23〉. 〈hal-01417618〉

Partager

Métriques

Consultations de la notice

174