O'Reilly logo

Handbook of Automated Reasoning by Andrei Voronkov, Alan J.A. Robinson

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required