Handbook of Automated Reasoning

5.2 Undecidability and other properties of simultaneous rigid E-unification

Gallier et al. [1987] introduced simultaneous rigid E-unification and asked whether this problem is decidable. Several papers published in 1988–1992 [Gallier, Narendran, Plaisted and Snyder 1988, Gallier, Narendran, Plaisted and Snyder 1990, Gallier et al. 1992, Gallier 1992, Goubault 1994] described faulty proofs of the decidability. Finally, in 1995 the problem was proved to be undecidable by Degtyarev and Voronkov [1995e] by reduction of monadic semi-unification whose undecidability was proved by Baaz [1993]. More comprehensive proofs of the undecidability appeared

1. in [Degtyarev and Voronkov 1995d , Degtyarev and Voronkov 1996f] by reduction of second-order ...