CONSTANT-ONLY MULTIPLICATIVE LINEAR LOGIC IS NP-COMPLETE

Linear logic is a resource-aware logic that is based on an analysis of the classical proof rules of contraction (copying) and weakening (thr owing away). In this paper we study the decision problem for the multi plicative fragment of linear logic without quantifiers or propositions : the constant-only case. We show that this fragment is NP-complete. E arlier work by Kanovich showed that propositional multiplicative linea r logic is NP-complete. With Natarajan Shankar, the first author devel oped a simplified proof for the propositional case. The structure of t his simplified proof is utilized here with a new encoding which uses o nly constants. The end products is the somewhat surprising result that simply evaluating expressions in true, false, and, or in multiplicati ve linear logic (1, perpendicular to. X and &) is NP-complete. By conv ersativity results not proven here, the NP-hardness of larger fragment s of linear logic follows.