Unification

A unifier is a predicate substitution applied on two different predicates to make them syntactically the same (i.e. have the same symbols). This is also the same as making two formulae logically equivalent. Unification is required in resolution in predicate logic.

Definition §

Unifier

Let $F$ and $G$ be two predicate formulae. Then, a unifier, $\theta$ is a predicate substitution such that:

$$F[\theta ]=G[\theta ]$$

If such a $\theta$ exists, then $F$ and $G$ are said to be unifiable. Here $=$ means syntactically the same (having the exact same symbols in the exact same order)

Most General Unifier §

Most General Unifier (MGU)

A most general unifier (MGU) $\theta$ is the ‘simplest’ unifier. It is a predicate substitution that satisfies:

• $\theta$ is a unifier
• Every other unifier, $\Phi$ can be expressed as a composition of $\theta$ with some other unifier $\tau$:

$$\Phi =\tau \circ \theta$$

The MGU is unique except in cases of variants (#todo )

#tosee Is there any way to prove that a substitution is a mgu?

Examples §

A lot of these examples rely on convention for naming terms, so see that first!

• $P(x)$ and $P(c)$ are unifiable with $\theta =\{x\mapsto c\}$. $P(x)[\theta ]\equiv P(c)[\theta ]$

  • $\theta$ is actually the most general unifier

• $P(x)$ and $P(y)$ have two MGUs : ${\theta }_1=\{x\mapsto y\}$ and ${\theta }_2=\{y\mapsto x\}$

  • $\Phi =\{x\mapsto c,y\mapsto c\}$ is not a MGU because it can be expressed as a composition: $\Phi =\{x\mapsto c\}\circ {\theta }_2$ or $\Phi =\{y\mapsto c\}\circ {\theta }_1$

Non-examples §

• $P(a)$ and $P(b)$ are not unifiable, because predicate substitution only applies to variables, not constants.

Uses §

• Compilers use unification to obtain the type signature of functions in coding