[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.