# 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.
1. only positive literals,
2. only two multiplicatives: tensor(multiplicative conjunction)
and linear implication -o
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.

```