ITU

Cut elimination in multifocused linear logic

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

View graph of relations

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.
Original languageEnglish
JournalElectronic Proceedings in Theoretical Computer Science. EPTCS
Volume176
Pages (from-to)24-33
Number of pages10
DOIs
Publication statusPublished - 2015
Close

    Research areas

  • Focusing, Linear logic, Cut elimination

Downloads

No data available

ID: 79510717