[Prev][Next][Index][Thread]

Complexity of Constant-Only Fragments of LL



 For ordinary logics (e.g. for classical or intuitionistic ones),
 their one-literal and, especially, constant-only fragments
 are essentially simpler than the corresponding full
 logics (with unrestricted number of literals.)

 The point is that the simulating of PSPACE-complete problems,
 a priori, requires unrestricted number of variables.
 For example, the proof of PSPACE-completeness of the implicative
 fragment of intuitionistic logic as well as of quantified Boolean
 formulas essentially uses unrestricted number of variables.

 Contrary to what might be expected, we prove that
 one-literal and even constant-only fragments of Linear
 Logic are of the same expressive power as the corresponding
 full parts of LL with infinite number of literals.

 In abbreviations like
    MLL,  MALL,  MELL,  MAELL
 LL indicates Propositional Linear Logic,
 M  indicates Multiplicatives: Tensor Product and Linear Implication,
 A  indicates Additives:       & and \oplus,
 E  indicates the storage operator !.

 Let us recall that
 1. MLL   is NP-complete (Kanovich, 1991).
 2. MALL  is PSPACE-complete
                         (Lincoln, Mitchell, Scedrov, and Shankar, 1990)
 3. MELL  can encode Petri Nets reachability.
 4. MAELL is undecidable (Lincoln, Mitchell, Scedrov, and Shankar, 1990)

 We consider One-literal parts of these fragments which contain
    (a) the only one positive literal p,
    (b) no other literals,
    (c) neither negative literals, nor constants, nor negations,
    (d) in the case E, the exponential ! is allowed to appear only
        outside of formulas.

 We proved the following results:
 1. One-literal MLL   is NP-complete (Kanovich, 1992).
 2. One-literal MALL  is PSPACE-complete (Kanovich, this message).
 3. One-literal MELL  can encode Petri Nets reachability.
                                    (Kanovich, this message).
 4. One-literal MAELL can directly simulate standard Minsky machines,
    and, hence, it is undecidable   (Kanovich, 1992, December).

 We consider Constant-only parts of the fragments of LL in question
 which contain
    (a) no literals at all,
    (b) the only constant \bottom,
    (c) neither other constants, nor negations,
    (d) only one multiplicative: linear implication,
    (e) in the case E, the exponential ! is allowed to appear only
        outside of formulas.

 The following results are proved:
 1. Constant-only MLL   is NP-complete (Lincoln and Winkler, 1992).
 2. Constant-only MALL  is PSPACE-complete (Kanovich, this message).
 3. Constant-only MELL  can encode Petri Nets reachability.
                                    (Kanovich, this message).
 4. Constant-only MAELL can directly simulate standard Minsky machines,
    and, hence, it is undecidable   (Kanovich, 1992, December).

 In order to establish PSPACE-hardness, we prove that the purely
 implicative fragment of intuitionistic logic can be directly
 simulated in One-literal MALL, as well as in Constant-only MALL.

 My best regards,
 Max Kanovich.