Cut Elimination in Multifocused Linear Logic
We study cut elimination for a multifocused variant of full linear logic in the sequent calculus. The multifocused normal form of proofs yields problems that do not appear in a standard focused system, related to the constraints in grouping rule instances in focusing phases. We show that cut elimina...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2015-02-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1502.04771v1 |
| _version_ | 1811240662099558400 |
|---|---|
| author | Taus Brock-Nannestad Nicolas Guenot |
| author_facet | Taus Brock-Nannestad Nicolas Guenot |
| author_sort | Taus Brock-Nannestad |
| collection | DOAJ |
| description | We study cut elimination for a multifocused variant of full linear logic in the sequent calculus. The multifocused normal form of proofs yields problems that do not appear in a standard focused system, related to the constraints in grouping rule instances in focusing phases. We show that cut elimination can be performed in a sensible way even though the proof requires some specific lemmas to deal with multifocusing phases, and discuss the difficulties arising with cut elimination when considering normal forms of proofs in linear logic. |
| first_indexed | 2024-04-12T13:24:10Z |
| format | Article |
| id | doaj.art-61689a53abff43f9b1834a8cfc1e01b9 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-12T13:24:10Z |
| publishDate | 2015-02-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-61689a53abff43f9b1834a8cfc1e01b92022-12-22T03:31:24ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802015-02-01176Proc. LINEARITY 2014243310.4204/EPTCS.176.3:9Cut Elimination in Multifocused Linear LogicTaus Brock-Nannestad0Nicolas Guenot1 INRIA & LIX, École Polytechnique IT University of Copenhagen We study cut elimination for a multifocused variant of full linear logic in the sequent calculus. The multifocused normal form of proofs yields problems that do not appear in a standard focused system, related to the constraints in grouping rule instances in focusing phases. We show that cut elimination can be performed in a sensible way even though the proof requires some specific lemmas to deal with multifocusing phases, and discuss the difficulties arising with cut elimination when considering normal forms of proofs in linear logic.http://arxiv.org/pdf/1502.04771v1 |
| spellingShingle | Taus Brock-Nannestad Nicolas Guenot Cut Elimination in Multifocused Linear Logic Electronic Proceedings in Theoretical Computer Science |
| title | Cut Elimination in Multifocused Linear Logic |
| title_full | Cut Elimination in Multifocused Linear Logic |
| title_fullStr | Cut Elimination in Multifocused Linear Logic |
| title_full_unstemmed | Cut Elimination in Multifocused Linear Logic |
| title_short | Cut Elimination in Multifocused Linear Logic |
| title_sort | cut elimination in multifocused linear logic |
| url | http://arxiv.org/pdf/1502.04771v1 |
| work_keys_str_mv | AT tausbrocknannestad cuteliminationinmultifocusedlinearlogic AT nicolasguenot cuteliminationinmultifocusedlinearlogic |