Unification
= Unification
Unification seeks substitutions for variables that make symbolic terms identical. First-order unification compares matching constructors recursively; an <occurs check> rejects substitutions that would make a variable contain itself.