🚀 go-pugleaf

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?

Thanks,
John Mitchell