Cut elimination in multifocused linear logic

Nicolas Guenot, Taus Brock-Nannestad

Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer review

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.
OriginalsprogEngelsk
TidsskriftElectronic Proceedings in Theoretical Computer Science. EPTCS
Vol/bind176
Sider (fra-til)24-33
Antal sider10
ISSN2075-2180
DOI
StatusUdgivet - 2015

Emneord

  • Focusing
  • Linear logic
  • Cut elimination

Fingeraftryk

Dyk ned i forskningsemnerne om 'Cut elimination in multifocused linear logic'. Sammen danner de et unikt fingeraftryk.

Citationsformater