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