Complexity bounds for sum-product logic via additive proof nets and Petri nets

Willem Heijltjes; Dominic Hughes

doi:10.1109/LICS.2015.18

Complexity bounds for sum-product logic via additive proof nets and Petri nets

Stanford University

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

5 Citations (SciVal)

204 Downloads (Pure)

Abstract

We investigate efficient algorithms for the additive fragment of linear logic. This logic is an internal language for categories with finite sums and products, and describes concurrent two-player games of finite choice. In the context of session types, typing disciplines for communication along channels, the logic describes the communication of finite choice along a single channel. We give a simple linear time correctness criterion for unit-free propositional additive proof nets via a natural construction on Petri nets. This is an essential ingredient to linear time complexity of the second author's combinatorial proofs for classical logic. For full propositional additive linear logic, including the units, we give a proof search algorithm that is linear-time in the product of the source and target formula, and an algorithm for proof net correctness that is of the same time complexity. We prove that proof search in first-order additive linear logic is NP-complete.

Original language	English
Title of host publication	Proceedings of the 30th ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015
Publisher	IEEE
Pages	80-91
Number of pages	12
ISBN (Print)	978-1-4799-8875-4
DOIs	https://doi.org/10.1109/LICS.2015.18
Publication status	Published - 10 Jul 2015
Event	30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015 - Kyoto, Japan Duration: 6 Jul 2015 → 10 Jul 2015

Publication series

Name	2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science
Publisher	IEEE
ISSN (Electronic)	1043-6871

Conference

Conference	30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015
Country/Territory	Japan
City	Kyoto
Period	6/07/15 → 10/07/15

Access to Document

10.1109/LICS.2015.18

ALL
(c) 2015 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other users, including reprinting/ republishing this material for advertising or promotional purposes, creating new collective works for resale or redistribution to servers or lists, or reuse of any copyrighted components of this work in other works
Submitted manuscript, 228 KB

Efficient and Natural Proof Systems
Guglielmi, A. (PI), Bruscoli, P. (CoI) & McCusker, G. (CoI)
Engineering and Physical Sciences Research Council
1/02/13 → 12/05/16
Project: Research council

Willem Heijltjes
- W.B.Heijltjesbath.acuk
- Department of Computer Science - Senior Lecturer
- Mathematical Foundations of Computation
Person: Research & Teaching

Cite this

Complexity bounds for sum-product logic via additive proof nets and Petri nets. / Heijltjes, Willem; Hughes, Dominic.
Proceedings of the 30th ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015. IEEE, 2015. p. 80-91 (2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science).

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

Heijltjes, W & Hughes, D 2015, Complexity bounds for sum-product logic via additive proof nets and Petri nets. in Proceedings of the 30th ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015. 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, pp. 80-91, 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015 , Kyoto, Japan, 6/07/15. https://doi.org/10.1109/LICS.2015.18

@inproceedings{0a5e72276e09413d821c802faef5d3d0,

title = "Complexity bounds for sum-product logic via additive proof nets and Petri nets",

abstract = "We investigate efficient algorithms for the additive fragment of linear logic. This logic is an internal language for categories with finite sums and products, and describes concurrent two-player games of finite choice. In the context of session types, typing disciplines for communication along channels, the logic describes the communication of finite choice along a single channel. We give a simple linear time correctness criterion for unit-free propositional additive proof nets via a natural construction on Petri nets. This is an essential ingredient to linear time complexity of the second author's combinatorial proofs for classical logic. For full propositional additive linear logic, including the units, we give a proof search algorithm that is linear-time in the product of the source and target formula, and an algorithm for proof net correctness that is of the same time complexity. We prove that proof search in first-order additive linear logic is NP-complete.",

author = "Willem Heijltjes and Dominic Hughes",

year = "2015",

month = jul,

day = "10",

doi = "10.1109/LICS.2015.18",

language = "English",

isbn = "978-1-4799-8875-4",

series = "2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science",

publisher = "IEEE",

pages = "80--91",

booktitle = "Proceedings of the 30th ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015",

address = "USA United States",

note = "30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015 ; Conference date: 06-07-2015 Through 10-07-2015",

}

TY - GEN

T1 - Complexity bounds for sum-product logic via additive proof nets and Petri nets

AU - Heijltjes, Willem

AU - Hughes, Dominic

PY - 2015/7/10

Y1 - 2015/7/10

N2 - We investigate efficient algorithms for the additive fragment of linear logic. This logic is an internal language for categories with finite sums and products, and describes concurrent two-player games of finite choice. In the context of session types, typing disciplines for communication along channels, the logic describes the communication of finite choice along a single channel. We give a simple linear time correctness criterion for unit-free propositional additive proof nets via a natural construction on Petri nets. This is an essential ingredient to linear time complexity of the second author's combinatorial proofs for classical logic. For full propositional additive linear logic, including the units, we give a proof search algorithm that is linear-time in the product of the source and target formula, and an algorithm for proof net correctness that is of the same time complexity. We prove that proof search in first-order additive linear logic is NP-complete.

AB - We investigate efficient algorithms for the additive fragment of linear logic. This logic is an internal language for categories with finite sums and products, and describes concurrent two-player games of finite choice. In the context of session types, typing disciplines for communication along channels, the logic describes the communication of finite choice along a single channel. We give a simple linear time correctness criterion for unit-free propositional additive proof nets via a natural construction on Petri nets. This is an essential ingredient to linear time complexity of the second author's combinatorial proofs for classical logic. For full propositional additive linear logic, including the units, we give a proof search algorithm that is linear-time in the product of the source and target formula, and an algorithm for proof net correctness that is of the same time complexity. We prove that proof search in first-order additive linear logic is NP-complete.

U2 - 10.1109/LICS.2015.18

DO - 10.1109/LICS.2015.18

M3 - Chapter in a published conference proceeding

SN - 978-1-4799-8875-4

T3 - 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science

SP - 80

EP - 91

BT - Proceedings of the 30th ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015

PB - IEEE

T2 - 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015

Y2 - 6 July 2015 through 10 July 2015

ER -

Complexity bounds for sum-product logic via additive proof nets and Petri nets

Abstract

Publication series

Conference

Access to Document

Fingerprint

Projects

Efficient and Natural Proof Systems

Profiles

Willem Heijltjes

Cite this