{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T14:22:37Z","timestamp":1787494957284,"version":"build-2736575974"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2016,3,2]],"date-time":"2016-03-02T00:00:00Z","timestamp":1456876800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>MLL proof equivalence is the problem of deciding whether two proofs in\nmultiplicative linear logic are related by a series of inference permutations.\nIt is also known as the word problem for star-autonomous categories. Previous\nwork has shown the problem to be equivalent to a rewiring problem on proof\nnets, which are not canonical for full MLL due to the presence of the two\nunits. Drawing from recent work on reconfiguration problems, in this paper it\nis shown that MLL proof equivalence is PSPACE-complete, using a reduction from\nNondeterministic Constraint Logic. An important consequence of the result is\nthat the existence of a satisfactory notion of proof nets for MLL with units is\nruled out (under current complexity assumptions). The PSPACE-hardness result\nextends to equivalence of normal forms in MELL without units, where the\nweakening rule for the exponentials induces a similar rewiring problem.<\/jats:p>","DOI":"10.2168\/lmcs-12(1:2)2016","type":"journal-article","created":{"date-parts":[[2016,11,21]],"date-time":"2016-11-21T08:47:11Z","timestamp":1479718031000},"source":"Crossref","is-referenced-by-count":5,"title":["Proof equivalence in MLL is PSPACE-complete"],"prefix":"10.46298","volume":"Volume 12, Issue 1","author":[{"given":"Willem","family":"Heijltjes","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robin","family":"Houston","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"25203","published-online":{"date-parts":[[2016,3,2]]},"reference":[{"key":"1131:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1625\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1625\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T16:08:14Z","timestamp":1681229294000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1625"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3,2]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-12(1:2)2016","relation":{"is-same-as":[{"id-type":"arxiv","id":"1510.06178","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1510.06178","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,3,2]]},"article-number":"1625"}}