Linear logic: Difference between revisions

Revision as of 11:33, 13 May 2020

Revision as of 14:09, 3 December 2020

Line 403:

* Multiplicative linear logic (MLL): only the multiplicative connectives. MLL entailment is [[NP-complete]], even restricting to [[Horn clauses]] in the purely implicative fragment,<ref>{{Cite conference| doi = 10.1109/LICS.1992.185533| conference = Seventh Annual IEEE Symposium on Logic in Computer Science, 1992. LICS '92. Proceedings| pages = 200–210| last = Kanovich| first = Max I.| title = Horn programming in linear logic is NP-complete| booktitle = Seventh Annual IEEE Symposium on Logic in Computer Science, 1992. LICS '92. Proceedings| date = 1992-06-22}}</ref> or to atom-free formulas.<ref>{{cite journal|first1=Patrick|last1=Lincoln|first2=Timothy|last2=Winkler|year=1994|title=Constant-only multiplicative linear logic is NP-complete|journal=Theoretical Computer Science|volume=135|pages=155–169|doi=10.1016/0304-3975(94)00108-1|doi-access=free}}</ref>

* 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]],<ref>{{Cite conference| conference = Tenth International Conference on Application and Theory of Petri Nets. Proceedings| pages = 174–191| last1 = Gunter| first1 = C. A.| last2 = Gehlot| first2 = V.| year = 1989}}</ref> 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)|TCS]],<ref>{{Cite journal| doi = 10.1016/j.tcs.2015.06.019| issn = 0304-3975| volume = 597| pages = 1–17| last = Bimbó| first = Katalin| title = The decidability of the intensional fragment of classical linear logic| journal = Theoretical Computer Science| date = 2015-09-13| doi-access = free}}</ref>, but was later shown to be erroneous.<ref>{{Cite journal| doi = 10.1016/j.tcs.2019.02.022| issn = 0304-3975| volume = 768| pages = 91–98| last = Straßburger| first = Lutz| title = On the decision problem for MELL| journal = Theoretical Computer Science| date = 2019-05-10| doi-access = free}}</ref>

* Affine linear logic (that is linear logic with weakening, an extension rather than a fragment) was shown to be decidable, in 1995.<ref>{{Cite conference| doi = 10.1109/LICS.1995.523283| citeseerx = 10.1.1.23.9226| conference = Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings| pages = 496–504| last = Kopylov| first = A. P.| title = Decidability of linear affine logic| booktitle = Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings| date = 1995-06-01}}</ref>