Decision problems for propositional linear logic: addendum
Date: Tue, 27 Mar 90 11:33:50 -0800
Addendum to "Decision Problems for propositional linear logic"
P. Lincoln, J. Mitchell, A. Scedrov, N. Shankar
We wish to add the following results to our recently announced work on
the decidability/complexity/undecidability of various fragments of
propositional linear logic:
1. Provability for the linear logic of (tensor, par, with, plus,
negation), i.e., the non-exponential fragment, is PSPACE-complete.
The PSPACE upper bound was claimed in our earlier announcement.
PSPACE-hardness is demonstrated by a transformation from the QBF
(Quantified Boolean Formula) validity problem.
2. Provability for multiplicative fragment of linear logic with
unrestricted weakening (Ketonen-Weyhrauch's "Direct logic") is
NP-complete. Membership in NP follows from a polynomial upper bound
on the size of cut-free proofs. NP-hardness is proved by a
transformation from the Vertex Cover problem.