Cut Elimination in Multifocused Linear Logic

descriptionPublicationkeyboard_double_arrow_right Article , Preprint , Conference object , Other literature type 16 Feb 2015Embargo end date: 01 Jan 2015 Denmark English Publisher:Open Publishing AssociationJournal:Electronic Proceedings in Theoretical Computer Science, volume 176, pages 24-33 (eissn: 2075-2180,

Copyright policy )

Authors: Guenot, Nicolas; Brock-Nannestad, Taus;

doi: 10.4204/eptcs.176.3 , 10.48550/arxiv.1502.04771

arXiv: 1502.04771

Cut Elimination in Multifocused Linear Logic

- Summary
- Subjects
- Metrics

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.

In Proceedings LINEARITY 2014, arXiv:1502.04419

Country

Denmark

Related Organizations

École Polytechnique
France
IT University of Copenhagen
Denmark

Keywords

FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Linear logic, QA75.5-76.95, 004, Logic in Computer Science (cs.LO), Electronic computers. Computer science, QA1-939, Cut elimination, Focusing, Mathematics

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	1
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average