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:
“In times like ours, where the growing complexity of life leaves us barely the time to read the newspapers, where the map of Europe has endured profound rearrangements and is perhaps on the brink of enduring yet others, where so many threatening and new problems appear everywhere, you will admit it may be demanded of a writer that he be more than a fine wit who makes us forget in idle and byzantine discussions on the merits of pure form ...”
—Marcel Proust (1871–1922)