Cut elimination in multifocused linear logic
- Nicolas Guenot,
- Taus Brock-Nannestad
- ,
- The French National Institute for Computer Science (INRIA),
- Computer Science Laboratory of the École polytechnique
Research Output:
Journal Article or Conference Article in Journal
Journal article
Peer-reviewOpen access
Publication Information
Output type
Research Output:
Journal Article or Conference Article in Journal
Journal article
Peer-reviewOriginal language
EnglishPages from-to (Number of pages)
Pages 24-33 (10 pages)Journal (Volume, Issue Number)
Electronic Proceedings in Theoretical Computer Science (Volume 176)Publication milestones
- Published - 2015
Publication status
Published - 2015
ISSN
2075-2180Publication IDs
- Scopus: 85020310544
Abstract
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.
Publication metrics
PlumX, opens in new tab
Mentions
1
Captures
3
Citations
2
Access to documents
Accepted author manuscript, 80.14 KB
Final published version
