Complexity questions on linear logic

To: types@theory.lcs.mit.edu, logic@theory.lcs.mit.edu, THEORYNT@vm1.nodak.edu
Date: Sat, 03 Feb 90 15:31:52 PST

Does anybody know anything about the complexity of decision
problems for propositional linear logic? I have a vague 
recollection of hearing something, but no concrete memory
of it. For example, what is the complexity of deciding whether
a propositional formula with connectives -o and ! is provable?
Or with tensor product added?

A specific question that has come up in type inference for 
linear logic is, given a propositional formula B, deciding
the set of formulas A such that A -o B is provable/valid.
In relevance logic terms, this is like the problem to 
deciding, for formula B, which A are relevant to inferring
B. Come to think of it, does anyone know if this is even
decidable for reasonable fragments of relevance logic R?

John Mitchell