[Prev][Next][Index][Thread]
Generalized Horn fragments of LL
Date: Sun, 24 Nov 1991 14:54:09 +0100
To: linear@cs.stanford.edu
Dear colleagues:
Now I am staying in Amsterdam (until December 15 1991)
and have an opportunity to use my temporary Dutch e-mail,
after December 15 I may use the following
e-mail: sergei@artemov.mian.su
With my best regards,
Sincerely yours,
Max Kanovich.
-----------------------------------------------------------------
I consider the smallest fragments of propositional linear
logic, namely, the Horn fragment and generalized Horn fragments
enriched by the two additive connectives and !.
Using a complete computational interpretation for these fragments,
the precise complexity level of them has been established.
Some notation conventions:
1. Henceforth, we use Xs, Ys, Ws and Zs to indicate simple
conjunctions, i. e. multiplicative conjunctions of a positive
number of positive literals.
2. A linear implication of the form (X -o Y) called Horn implication.
3. We study generalized Horn implications, namely,
(+)-Horn implications of the form (X -o (Y_1 (+) Y_2)), and
&-Horn implication of the form ((X_1 -o Y_1) & (X_2 -o Y_2)).
4. A Horn sequent is a sequent of the form G, W |- Z,
where G is a multiset consisting of Horn implications.
5. Similar to the previous item, we define (+)-Horn sequents,
&-Horn sequents etc. E. g. a (+,&)-Horn sequent is of the
form G, W |- Z, where G is a multiset consisting of Horn
implications, (+)-Horn implications and &-Horn implications.
6. For a Horn sequent G, W |- Z, the sequent !G, W |- Z is
called !-Horn sequent. (By !G we denote the multiset that
is constructed from a multiset G by writing down the exclamation
mark ! before each formula of G.)
7. Similar to the previous items, (!,+)-Horn sequents, (!,&)-Horn
sequents etc. are defined.
Considering all possible combinations, I can prove that
( HLL) The Horn fragment of linear logic is NP-complete.
As a corollary, the purely implicative fragment of linear logic
(where we may use only positive literals and linear implications)
is also NP-complete.
(+HLL) The (+)-Horn fragment of linear logic is NP-complete.
(&HLL) The &-Horn fragment of linear logic is NP-complete.
(+&HLL) The (+,&)-Horn fragment of linear logic is PSPACE-complete.
Following the idea of the encoding proposed in Chapter 2 of
[LMSS 90], we can directly transform a quantified Boolean formula
into the corresponding (+,&)-Horn sequent.
Besides, we prove that the (+,&)-Horn fragment is solvable
in deterministic linear space.
(!HLL) The !-Horn fragment of linear logic is decidable. Moreover,
the decision problem for !-Horn sequents is polynomially
equivalent to the reachability problem for Petri nets.
(!+HLL) The (!,+)-Horn fragment of linear logic is undecidable.
(It follows from [LMSS 90])
(!&HLL) The (!,&)-Horn fragment of linear logic is decidable, (and
its decision problem is exactly equivalent to the
reachability problem for Petri nets).
For linear logic with the Weakening rule, similar and non-similar
results have been obtained:
( HLW) The Horn fragment of linear logic with weakening is NP-complete.
(+HLW) The (+)-Horn fragment of linear logic with weakening is
PSPACE-complete.
(&HLW) The &-Horn fragment of linear logic with weakening is NP-complete.
(+&HLW) The (+,&)-Horn fragment of linear logic with weakening is
PSPACE-complete.
The (+,&)-Horn fragment is solvable in deterministic linear space.
(!HLW) The !-Horn fragment of linear logic with weakening is decidable.
(!&HLW) The (!,&)-Horn fragment of linear logic with weakening is decidable.
In relation with Patrick Lincoln e-message
"Two surprises to me are how little first order quantifiers and
unrestricted weakening effect the expressiveness of fragments
of linear logic."
it could be noted that adding (+) to rudimentary linear logic along
with the Weakening rule changes the picture:
according to cases (+HLL) and (+HLW), for (+)-Horn sequents,
the problem of their derivability in linear logic with weakening
turns out to be PSPACE-complete.
In conclusion, I have got some partial results related to the
decision problem for multiplicatives plus !:
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.
(Adding Weakening does not change this result).
A part of these results is contained in
The ITLI Prepublication Series of University of Amsterdam:
1991, ITLI-X-91-14, Max I. Kanovich, "The Horn Fragment of
Linear Logic is NP-Compete",