Linear Logic - Decidability/complexity of Entailment

Decidability/complexity of Entailment

The entailment relation in full CLL is undecidable. Fragments of CLL are often considered, for which the decision problem is more subtle:

  • Multiplicative linear logic (MLL): only the multiplicative connectives. MLL entailment is NP-complete.
  • Multiplicative-additive linear logic (MALL): only multiplicatives and additives (i.e., exponential-free). MALL entailment is PSPACE-complete.
  • Multiplicative-exponential linear logic (MELL): only multiplicatives and exponentials. The decidability of MELL entailment is currently open.

Read more about this topic:  Linear Logic

Famous quotes containing the word complexity:

    It is not only their own need to mother that takes some women by surprise; there is also the shock of discovering the complexity of alternative child-care arrangements that have been made to sound so simple. Those for whom the intended solution is equal parenting have found that some parents are more equal than others.
    Elaine Heffner (20th century)