Robinson unification algorithm

The Robinson unification algorithm solves equations between first-order terms by finding a substitution making them identical. Repeatedly delete equal terms, decompose equal function symbols into argument equations, reject incompatible symbols, and substitute a variable by its proposed term. The occurs check rejects $x=f(x)$ for finite-term unification, since no finite term equals a proper term containing itself. For $f(x,a)=f(b,y)$ it returns $x\mapsto b$, $y\mapsto a$. Successful finite-term unification yields a most general unifier: every other unifier is obtained by further substitution. Implementations that omit the occurs check instead admit a different cyclic-term interpretation.