[Prev][Next][Index][Thread]
Re: Generalized Horn fragments of LL
Date: Mon, 25 Nov 1991 15:47:54 +0100
To: linear@cs.stanford.edu
[note from LINEAR moderator:
Below I abbreviate a dialogue between myself and Max Kanovich.
Also, Dirk Roorda'a email address is: roorda@fwi.uva.nl
]
> > Date: Sun, 24 Nov 1991 14:54:09 +0100
> > From: maxk@cwi.nl
> > To: linear@cs.stanford.edu
> > ...
> > For sequents of the form !G, H, W |- Z ,
> > where the multiset G contains Horn implications and &-Horn implications,
> > and the multiset H may contain arbitrary formulas having no occurrences
> > of (+), & and !,
> > their derivability problem is decidable.
>
> From: Patrick Lincoln <lincoln@Theory.Stanford.EDU>
> Perhaps I could ask how "arbitrary" the formulas are?
> ...
Thanks You for indicating the point of possible misunderstanding
in my e-mail announcement related to generalized Horn fragments
of LL.
The point is that I have used implicitly the following conventions.
We have had:
1. only positive literals,
2. only two multiplicatives: tensor(multiplicative conjunction)
and linear implication -o
3. only two additives: additive conjunction & and
additive disjunction (+),
4. only one exponential: !
Taking into account these conventions, my assertion
"a formula f has no occurrences of (+), & and !" has meant exactly
"a formula f may include only positive literals, tensors and -o".
> ----------------------------
> From: Patrick Lincoln <lincoln@Theory.Stanford.EDU>
> Could you mention briefly how you show that +HLL is in NP, and
> how +HLW is PSPACE-Hard? These are very interesting results,
> in that they show, as you mention, a difference in expressiveness.
> I would have guessed that these logics would have the same complexity.
As to your questions how I show that the (+)-Horn fragment of linear
logic is in NP and how the (+)-Horn fragment of linear logic with
weakening is PSPACE-Hard,
a. (+)-Horn sequents in linear logic are reduced to Horn sequents in it,
b. I have used the corresponding embedding of quantifiered Boolean
formulas into the (+)-Horn fragment of linear logic with
weakening.
It could be pointed out that, at least for (+)-Horn sequents, adding
the Weakening rule to LL is 'equivalent to' introducing &, so that
the (+)-Horn fragment of linear logic with weakening is of the
same complexity as the (+,&)-Horn fragment of linear logic.
With my best regards,
Sincerely yours,
Max Kanovich.