Plaisted, David A. Max Planck Society;
Chadha, R., & Plaisted, D. A. (1994). Correctness of unification without occur check in Prolog. Journal of Logic Programming, 18(2), 99-122.