Unification

Remarks

If $s$ and $t$ have a unifier, then they have a most general unifier, unique up to renaming of variables, and Robinson's algorithm finds it. The same notions apply to finite sets of pairs of terms, which are unified simultaneously. In $E$-unification one asks instead for $s\theta \approx t\theta$ to follow from a set $E$ of identities.

Example: $s = f(x, b)$ and $t = f(a, y)$, with constants $a, b$, have the unifier $\theta = \set{x \mapsto a, \ y \mapsto b}$. Indeed $s\theta = f(a, b) = t\theta$, and $\theta$ is most general because every unifier must send $x$ to $a$ and $y$ to $b$.

Non-example: $x$ and $f(x)$ have no unifier. For every substitution $\theta$, the term $f(x)\theta = f(x\theta)$ has one more symbol than $x\theta$, so they are never identical.