Cut elimination in multifocused linear logic
- Nicolas Guenot,
- Taus Brock-Nannestad
- ,
- Inria,
- Computer Science Laboratory of the École polytechnique
Publikation:
Artikel i tidsskrift og konference artikel i tidsskrift
Tidsskriftartikel
Peer-reviewOpen Access
Publikation information
Produktionstype
Publikation:
Artikel i tidsskrift og konference artikel i tidsskrift
Tidsskriftartikel
Peer-reviewOriginalsprog
EngelskSider fra-til (Antal sider)
Sider 24-33 (10 sider)Tidsskrift (Bind, Nummer)
Electronic Proceedings in Theoretical Computer Science (Bind 176)Publikationsmilepæle
- Udgivet - 2015
Publikationsstatus
Udgivet - 2015
ISSN
2075-2180Publication IDs
- Scopus: 85020310544
Resume
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.
Metrikker
PlumX, åbner i en ny fane
Hentninger
3
Citationer
2
Adgang til dokumenter
Accepteret manuskript, 80.14 KB
Forlagets udgivne version
