Voir la figure 2 pour un algorithme d'unification retournant une forme triangulaire, dans le style de Martelli et Montanari [MM82]. L'algorithme fonctionne en transformant des couples (F,s), où F est un ensemble ou un multi-ensemble de paires de termes (représentées comme des équations formelles non orientées entre termes) qui doivent être unifiées simultanément, et s est la forme triangulaire du mgu en cours de construction. En pratique, les multi-ensembles sont codés sous forme de listes, où l'ordre des éléments est jugé sans importance.
Figure 2: Règles d'unification