June 2001
Intermediate to advanced
2128 pages
82h 43m
English
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 ...
Read now
Unlock full access