"On the construction of unifying terms modulo a set of substitutions."

Steffen Lange (1987)
a service of Schloss Dagstuhl - Leibniz Center for Informatics