No proof nets for MLL with units: Proof equivalence in MLL is PSPACE-complete

W. Heijltjes, Robin Houston

Research output: Chapter in Book/Report/Conference proceedingConference contribution

17 Citations (Scopus)
101 Downloads (Pure)

Abstract

MLL proof equivalence is the problem of deciding whether two proofs in multiplicative linear logic are related by a series of inference permutations. It is also known as the word problem for *-autonomous categories. Previous work has shown the problem to be equivalent to a rewiring problem on proof nets, which are not canonical for full MLL due to the presence of the two units. Drawing from recent work on reconfiguration problems, in this paper it is shown that MLL proof equivalence is PSPACE-complete, using a reduction from Nondeterministic Constraint Logic. An important consequence of the result is that the existence of a satisfactory notion of proof nets for MLL with units is ruled out (under current complexity assumptions).
Original languageEnglish
Title of host publicationProceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014
Place of PublicationNew York
PublisherAssociation for Computing Machinery
Number of pages10
ISBN (Print)9781450328869
DOIs
Publication statusPublished - 2014
EventJoint Meeting of the 23rd Annual EACSL Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/ IEEE Symposium on Logic in Computer Science, LICS 2014 - Vienna , Austria
Duration: 14 Jul 201418 Jul 2014

Conference

ConferenceJoint Meeting of the 23rd Annual EACSL Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/ IEEE Symposium on Logic in Computer Science, LICS 2014
CountryAustria
CityVienna
Period14/07/1418/07/14

Fingerprint Dive into the research topics of 'No proof nets for MLL with units: Proof equivalence in MLL is PSPACE-complete'. Together they form a unique fingerprint.

Cite this