Unifikation--Algorithmus

mgu(s, t) nach Fallunterscheidung

• s ist Variable: ...
• t ist Variable: symmetrisch
• s = (s₁→s₂) und t = (t₁→t₂): ...

mgu :: Term -> Term -> Maybe Substitution