DocumentCode :
728963
Title :
Complexity Bounds for Sum-Product Logic via Additive Proof Nets and Petri Nets
Author :
Heijltjes, Willem ; Hughes, Dominic J. D.
fYear :
2015
fDate :
6-10 July 2015
Firstpage :
80
Lastpage :
91
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.
Keywords :
Petri nets; computational complexity; formal logic; game theory; search problems; NP-complete; Petri nets; additive proof nets; classical logic; combinatorial proof; complexity bound; first-order additive linear logic; linear time complexity; linear time correctness criterion; natural construction; proof net correctness; proof search algorithm; propositional additive linear logic; session type; sum-product logic; two-player game; typing discipline; unit-free propositional additive proof net; Additives; Games; Petri nets; Semantics; Syntactics; Time complexity; Petri nets; additive linear logic; linear logic; proof complexity; sumproduct categories;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science (LICS), 2015 30th Annual ACM/IEEE Symposium on
Conference_Location :
Kyoto
ISSN :
1043-6871
Type :
conf
DOI :
10.1109/LICS.2015.18
Filename :
7174872
Link To Document :
بازگشت