[Prev][Next][Index][Thread]
Complexity of LL fragments
To: linear@cs.stanford.edu
Organization: Steklov Mathematical Institute
Phone: (7095) 135 1569
Fax: (7095) 135 0555
Date: Tue, 14 Jul 92 16:40:46 +0300 (MSD)
We show that, contrary to ordinary logical systems, very simple fragments
of Linear Logic are of very high complexity.
We estimate the decision complexity of the simplest fragments of
the Multiplicative Fragment of Girard's Linear Logic that contain a
limited (and extremely small) number of literals.
The Multiplicative Fragment of LL and even the Horn Fragment of LL
are NP-complete (M.Kanovich, 1991; see also LICS'92).
P.Lincoln and T.Winkler recently proved NP-completeness for the
Multiplicative Fragment of LL with constants, but without any literals.
We prove that the following fragments are NP-complete:
1. The Pure Implicative Fragment in which we use
only linear implications
and only ONE positive literal
(this fragment does not contain any constants or negations).
2. The Pure Implicative Fragment in which we use
only linear implications
and only ONE constant \bottom
(this fragment does not contain any literals).
3. The Horn Fragment of Linear Logic in which we use
only TWO positive literals.
(See the definition of the Horn Fragment of LL and the idea of proving
NP-completeness of the Horn fragment with TWO literals
in the paper 'Horn Programming in Linear Logic is NP-complete'
by Max I. Kanovich, published in LICS'92.)
4. The Horn Fragment of Linear Logic in which we use
only ONE positive literal and the constant \bottom.
The Horn fragment of LL containing only ONE literal is proved to be
in P (in fact, it is linear time recognizable).
Best regards, Max Kanovich.