Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!uunet!tut.cis.ohio-state.edu!ucbvax!CS.STANFORD.EDU!jcm
From: jcm@CS.STANFORD.EDU ("John C. Mitchell")
Newsgroups: comp.theory
Subject: Complexity questions on linear logic
Message-ID: <9002032331.AA02070@iswim.stanford.EDU>
Date: 5 Feb 90 21:44:00 GMT
Sender: daemon@ucbvax.BERKELEY.EDU
Reply-To: "John C. Mitchell" <jcm%cs.stanford.edu@VM1.NoDak.EDU>
Lines: 17

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