How hard is it to tell when two proofs are equivalent in MLL?

Robin Houston

There is an elegant and efficient procedure for deciding whether two proofs in multiplicative linear logic are equivalent: convert both of them into the graphical form of a *proof net*, and compare the proof nets for equality. But this only works if the logical units 1 and ⟂ are excluded. Recent work with Willem Heijltjes has established that the presence of the units makes proof equivalence hard to decide: the problem is PSPACE-complete.