jcm@CS.STANFORD.EDU ("John C. Mitchell") (02/06/90)
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