##
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.