Decision problems for propositional linear logic: addendum

• To: types
• Subject: Decision problems for propositional linear logic: addendum
• From: Natarajan Shankar <shankar@csl.sri.com>
• Date: Tue, 27 Mar 90 16:14:10 EST
• Sender: meyer@theory.lcs.mit.edu

Return-Path: <shankar@argon.csl.sri.com>
Date: Tue, 27 Mar 90 11:33:50 -0800
Cc: logmtc@sail.stanford.edu

     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.

• Prev: Decision problems for propositional linear logic
• Next: Workshop: Structuring Disciplines for Logic Programming
• Index(es):
  • Main
  • Thread