Conflict nets: efficient locally canonical MALL proof nets

Dominic Hughes, Willem Heijltjes

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Citations (Scopus)
94 Downloads (Pure)

Abstract

Proof nets for MLL (unit-free multiplicative linear logic) and (unit-free additive linear logic) are graphical abstractions of proofs which are efficient (proofs translate in linear time) and canoni- cal (invariant under rule commutation). This paper solves a three- decade open problem: are there efficient canonical proof nets for MALL (unit-free multiplicative-additive linear logic)?
Honouring MLL and ALL canonicity, in which all commutations are strictly local proof-tree rewrites, we define local canonicity for MALL: invariance under local rule commutation. We present new proof nets for MALL, called conflict nets, which are both efficient and locally canonical.
Original languageEnglish
Title of host publicationProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016
Place of PublicationNew York, U. S. A.
PublisherAssociation for Computing Machinery
Pages437-446
Number of pages10
ISBN (Print)9781450343916
DOIs
Publication statusPublished - 2 Jul 2016
Event31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016 - New York, USA United States
Duration: 5 Jul 20168 Jul 2016

Publication series

NameProceedings - Symposium on Logic in Computer Science
PublisherIEEE
ISSN (Electronic)2575-5528

Conference

Conference31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016
CountryUSA United States
CityNew York
Period5/07/168/07/16

Fingerprint Dive into the research topics of 'Conflict nets: efficient locally canonical MALL proof nets'. Together they form a unique fingerprint.

  • Projects

  • Profiles

    No photo of Willem Heijltjes

    Cite this

    Hughes, D., & Heijltjes, W. (2016). Conflict nets: efficient locally canonical MALL proof nets. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016 (pp. 437-446). (Proceedings - Symposium on Logic in Computer Science). Association for Computing Machinery. https://doi.org/10.1145/2933575.2934559