= Unification
<Unification> finds a <substitution> making given <first-order terms> syntactically identical. In <first-order unification>, a <substitution> replaces <variables> by <first-order terms> while leaving <function symbols> fixed. A <most general unifier> captures the necessary identifications: every other <unifier> follows by a further <substitution>.<A Machine-Oriented Logic Based on the Resolution Principle by J. A. Robinson>[sections 5.3–5.9 and the unification theorem]{ref}
For example, $f(x,g(y))$ and $f(g(z),g(a))$ have <most general unifier> $\{x\mapsto g(z),y\mapsto a\}$. The <variable> $z$ remains free; assigning it a particular <first-order term> gives a more specific <unifier>. Requiring $f(x,x)=f(a,b)$ forces both $x=a$ and $x=b$, so distinct <constant symbols> $a,b$ make it impossible.
Syntactic identity is essential. With addition treated as a binary <function symbol>, the <first-order terms> $x+0$ and $x$ are different even though their values agree under ordinary <arithmetic>. <Equational unification> incorporates specified identities and is a different problem. For finite <first-order terms>, the <occurs check> rejects $x=f(x)$: a finite <first-order term> cannot equal one of its proper <subterms>. <Unification> makes <resolution> possible by aligning <atomic formulas> before inference.
Back to article page
