Mechanical synthesis of a unification algorithm in PowerEpsilon. - Ming-Yuan Zhu; Xiao-Bai Mo (COMPSAC, 1995)