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

Willem Heijltjes, Dominic Hughes

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

5 Citations (Scopus)
125 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 languageEnglish
Title of host publicationProceedings of the 30th ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015
PublisherIEEE
Pages80-91
Number of pages12
ISBN (Print)978-1-4799-8875-4
DOIs
Publication statusPublished - 10 Jul 2015
Event30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015 - Kyoto, Japan
Duration: 6 Jul 201510 Jul 2015

Publication series

Name2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science
PublisherIEEE
ISSN (Electronic)1043-6871

Conference

Conference30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015
CountryJapan
CityKyoto
Period6/07/1510/07/15

Fingerprint Dive into the research topics of 'Complexity bounds for sum-product logic via additive proof nets and Petri nets'. Together they form a unique fingerprint.

  • Projects

  • Profiles

    No photo of Willem Heijltjes

    Cite this

    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 (pp. 80-91). (2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science). IEEE. https://doi.org/10.1109/LICS.2015.18