Conflict nets: efficient locally canonical MALL proof nets

Dominic Hughes; Willem Heijltjes

doi:10.1145/2933575.2934559

Conflict nets: efficient locally canonical MALL proof nets

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

9 Citations (SciVal)

233 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 language	English
Title of host publication	Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016
Place of Publication	New York, U. S. A.
Publisher	Association for Computing Machinery
Pages	437-446
Number of pages	10
ISBN (Print)	9781450343916
DOIs	https://doi.org/10.1145/2933575.2934559
Publication status	Published - 2 Jul 2016
Event	31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016 - New York, USA United States Duration: 5 Jul 2016 → 8 Jul 2016

Publication series

Name	Proceedings - Symposium on Logic in Computer Science
Publisher	IEEE
ISSN (Electronic)	2575-5528

Conference

Conference	31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016
Country/Territory	USA United States
City	New York
Period	5/07/16 → 8/07/16

Access to Document

10.1145/2933575.2934559

final_version.PDF
© ACM, 2016. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, (2016), pp. 437-446. https://doi.org/10.1145/2933575.2934559
Accepted author manuscript, 242 KB

Cite this

Conflict nets: efficient locally canonical MALL proof nets. / Hughes, Dominic; Heijltjes, Willem.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016. New York, U. S. A.: Association for Computing Machinery, 2016. p. 437-446 (Proceedings - Symposium on Logic in Computer Science).

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

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. Proceedings - Symposium on Logic in Computer Science, Association for Computing Machinery, New York, U. S. A., pp. 437-446, 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016, New York, USA United States, 5/07/16. https://doi.org/10.1145/2933575.2934559

@inproceedings{c879e168640a4000938dafc9e64dbaaf,

title = "Conflict nets: efficient locally canonical MALL proof nets",

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.",

author = "Dominic Hughes and Willem Heijltjes",

year = "2016",

month = jul,

day = "2",

doi = "10.1145/2933575.2934559",

language = "English",

isbn = "9781450343916",

series = "Proceedings - Symposium on Logic in Computer Science",

publisher = "Association for Computing Machinery",

pages = "437--446",

booktitle = "Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016",

address = "USA United States",

note = "31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016 ; Conference date: 05-07-2016 Through 08-07-2016",

}

TY - GEN

T1 - Conflict nets

T2 - 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016

AU - Hughes, Dominic

AU - Heijltjes, Willem

PY - 2016/7/2

Y1 - 2016/7/2

N2 - 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.

AB - 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.

UR - http://dx.doi.org/10.1145/2933575.2934559

U2 - 10.1145/2933575.2934559

DO - 10.1145/2933575.2934559

M3 - Chapter in a published conference proceeding

SN - 9781450343916

T3 - Proceedings - Symposium on Logic in Computer Science

SP - 437

EP - 446

BT - Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016

PB - Association for Computing Machinery

CY - New York, U. S. A.

Y2 - 5 July 2016 through 8 July 2016

ER -

Conflict nets: efficient locally canonical MALL proof nets

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Efficient and Natural Proof Systems

COMPLEXITY AND NON-DETERMINISM IN DEEP INFERENCE

Willem Heijltjes

Cite this

Conflict nets: efficient locally canonical MALL proof nets

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Projects

Efficient and Natural Proof Systems

COMPLEXITY AND NON-DETERMINISM IN DEEP INFERENCE

Profiles

Willem Heijltjes

Cite this