Constant-only multiplicative linear logic is NP-complete (Q1342254)

The paper considers the decision problem for the multiplicative fragment of linear logic without quantifiers or propositions: the constant only case. The authors show that this fragment is NP-complete. Three independent logics are considered: full propositional linear logic, restricted to multiplicative connectives and constants, and the constant only fragment. These calculi are considered as Gentzen-style sequent calculi since 3-Partition and 432-Partition are equivalent problems, so the authors encode an NP-complete problem, 432-Partition in the constant only fragment of linear logic restricted to multiplicative connectives and constants, and show this encoding is sound and complete. The decision problem for constant-only multiplicative linear logic is NP-complete. The complexity of most of the larger fragments of linear logic has already been completely characterized by P. Lincoln, J. Mitchell, A. Scedrov and N. Shankar.