Content deleted Content added
→Decidability/complexity of entailment: rm claim with bogus reference. https://dblp.org/db/conf/apn/apn1989.html lists nothing matching from that conference, and https://dblp.org/pid/g/CarlAGunter.html lists only an unrelated paper with Gehlot. |
restoring remark with better reference to tech report |
||
Line 484:
* 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| book-title = Seventh Annual IEEE Symposium on Logic in Computer Science, 1992. LICS '92. Proceedings| date = 1992-06-22| isbn = 0-8186-2735-2}}</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 tech report|last1 = Gunter| first1 = C. A.| last2 = Gehlot| first2 = V.| title=Nets as Tensor Theories|institution=University of Pennsylvania|number=MS-CIS-89-68|year = 1989|url=http://seclab.illinois.edu/wp-content/uploads/2011/04/GunterG89.pdf}}</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)|Theoretical Computer Science]]'',<ref>{{Cite journal| doi = 10.1016/j.tcs.2015.06.019| issn = 0304-3975| volume = 597| pages = 1–17| last = Bimbó| first = Katalin|author-link= Katalin Bimbó | 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| book-title = Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings| date = 1995-06-01| isbn = 0-8186-7050-9}}</ref>
| |||