Fassbender, H. and Vogler, H. 1994. A universal unification algorithm based on unification-driven leftmost outermost narrowing. Acta Cybernetica. 11, 3 (Jan. 1994), 139-167.