Single versus simultaneous equational unification and equational unification for variable-permuting theories

A clear distinction is made between the (elementary) unification problem where there is only one pair of terms to be unified, and the simultaneous unification problem, where many such pairs have to be unified simultaneously - it is shown that there exists a finite, depth-reducing, linear, and confluent term-rewriting system R such that the (single) equational unification problem mod R is decidable, while the simultaneous equational unification problem mod R is undecidable. Also a finite set ℰ of variable-permuting equations is constructed such that equational unification is undecidable mod ℰ, thus settling an open problem. The equational matching problem for variable-permuting theories is shown to be PSPACE-complete.