Editing Linear logic (section)

==Decidability/complexity of entailment==

The [[entailment]] relation in full CLL is [[Undecidable problem|undecidable]].{{refn|name=Lincoln+92|For this result and discussion of some of the fragments below, see: {{harvtxt|Lincoln|Mitchell|Scedrov|Shankar|1992}}}} When considering fragments of
CLL, the decision problem has varying complexity:

* Multiplicative linear logic (MLL): only the multiplicative connectives.  MLL entailment is [[NP-complete]], even restricting to [[Horn clauses]] in the purely implicative fragment,{{sfn|Kanovich|1992}} or to atom-free formulas.{{sfn|Lincoln|Winkler|1994}}
* Multiplicative-additive linear logic (MALL): only multiplicatives and additives (i.e., exponential-free).  MALL entailment is [[PSPACE-complete]].<ref name="Lincoln+92" />
* Multiplicative-exponential linear logic (MELL): only multiplicatives and exponentials. By reduction from the reachability problem for [[Petri nets]],{{sfn|Gunter|Gehlot|1989}} MELL entailment must be at least [[EXPSPACE|EXPSPACE-hard]], although decidability itself has had the status of a longstanding open problem. In 2015, a proof of decidability was published in the journal ''[[Theoretical Computer Science (journal)|Theoretical Computer Science]]'',{{sfn|Bimbó|2015}} but was later shown to be erroneous.{{sfn|Straßburger|2019}}
* Affine linear logic (that is linear logic with weakening, an extension rather than a fragment) was shown to be decidable, in 1995.{{sfn|Kopylov|1995}}