Canonical Sequent Proofs via Multi-Focusing Export

@incollection{citeulike:5916648, abstract = {The sequent calculus admits many proofs of the same conclusion that differ only by trivial permutations of inference rules. In order to eliminate this ” bureaucracy” from sequent proofs, deductive formalisms such as proof nets or natural deduction are usually used instead of the sequent calculus, for they identify proofs more abstractly and geometrically. In this paper we recover permutative canonicity directly in the cut-free sequent calculus by generalizing focused sequent proofs to admit multiple foci, and then considering the restricted class of maximally multi-focused proofs. We validate this definition by proving a bijection to the well-known proof-nets for the unit-free multiplicative linear logic, and discuss the possibility of a similar correspondence for larger fragments.}, author = {Chaudhuri, Kaustuv and Miller, Dale and Saurin, Alexis}, citeulike-article-id = {5916648}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-0-387-09680-3_26}, citeulike-linkout-1 = {http://www.springerlink.com/content/x624g1763277657k}, doi = {10.1007/978-0-387-09680-3_26}, journal = {Fifth Ifip International Conference On Theoretical Computer Science – Tcs 2008}, keywords = {focusing, linear-logic, multi-focusing}, pages = {383--396}, posted-at = {2009-10-09 16:38:12}, priority = {0}, title = {Canonical Sequent Proofs via Multi-Focusing}, url = {http://dx.doi.org/10.1007/978-0-387-09680-3_26}, year = {2008} }

TY - CHAP ID - citeulike:5916648 L3 - citeulike-article-id:5916648 N2 - The sequent calculus admits many proofs of the same conclusion that differ only by trivial permutations of inference rules. In order to eliminate this “bureaucracy” from sequent proofs, deductive formalisms such as proof nets or natural deduction are usually used instead of the sequent calculus, for they identify proofs more abstractly and geometrically. In this paper we recover permutative canonicity directly in the cut-free sequent calculus by generalizing focused sequent proofs to admit multiple foci, and then considering the restricted class of maximally multi-focused proofs. We validate this definition by proving a bijection to the well-known proof-nets for the unit-free multiplicative linear logic, and discuss the possibility of a similar correspondence for larger fragments. JF - Fifth Ifip International Conference On Theoretical Computer Science – Tcs 2008 EP - 396 TI - Canonical Sequent Proofs via Multi-Focusing SP - 383 KW - focusing KW - linear-logic KW - multi-focusing AU - Chaudhuri, Kaustuv AU - Miller, Dale AU - Saurin, Alexis PY - 2008/// UR - http://dx.doi.org/10.1007/978-0-387-09680-3_26 ER -