Socher-Ambrosius, Rolf Programming Logics, MPI for Informatics, Max Planck Society;
https://rdcu.be/dttYk (Publisher version)
Socher-Ambrosius, R. (1994). A Refined Version of General E-Unification. In A. Bundy (Ed.), Automated Deduction - CADE-12 (pp. 665-677). Berlin, Germany: Springer.