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:

    The price we pay for the complexity of life is too high. When you think of all the effort you have to put in—telephonic, technological and relational—to alter even the slightest bit of behaviour in this strange world we call social life, you are left pining for the straightforwardness of primitive peoples and their physical work.
    Jean Baudrillard (b. 1929)