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.
New to topics? Read the docs here!