Unification

Recall that in considering the resolution inference rule (and various specific strategies employing it) in Chapter 2 we restricted our attention to the propositional case. This meant that progress revolved around two or more contradictory propositional variables. For example, recall the form of binary resolution for the propositional case:

$$\begin{array}{c} \phi \vee \psi \quad \neg\psi \vee \chi\\ \hline \phi \vee \chi\\ \end{array}$$

Note that in this schema $\psi$ and $\neg \psi$ ``cancel" each other out, and note that they do so by being contradictories. The same basic idea is present in resolution applied to the case of first-order formula, but in this case cancellation is extended so that two literals cancel if they can be unified so as to contradict each other. (Resolution-based identity rules will require a more subtle notion than contradictory literals.) We now explain unification.

We begin with the concept of a substitution or binding list. Such a thing is simply a set of ordered pairs, the first element of which is a variable and the second of which is a term. A substitution must satisfy the following two conditions.

1.

Each variable is paired with at most one term.

2.

No variable paired with a term occurs within any of the terms.

Here is an example of a substitution:^4.2

$$\{x/a, y/f(b), z/w\}.$$

On the other hand, the following set does not qualify; make sure you see why.

$$\{x/f(y), y/b\}.$$

Now we can apply a substitution or binding list to a first-order term or formula to yield a new expression. This process is really quite simple: we simply replace variables in the term or formula with terms paired with these variables in the substitution. We write

$$\phi \sigma$$

to indicate the result of applying the substitution $\sigma$ to formula (or term) $\phi$. Here is an example:

$$R(x,x,y,v)\{x/a, y/f(b), z/w\} = R(a,a,f(b),v)$$

A substition $\sigma$ is distinct from a substitution $\tau$ iff no variable paired with a term in $\sigma$ occurs in $\tau$. Given a substitution $\sigma$ and a distinct substitution $\tau$, the composition of $\tau$ with $\sigma$, written $\sigma \tau$) is the substitution produced by apploying $\tau$ to the terms of $\sigma$ and then adding to $\sigma$ the bindings from $\tau$. Here is an example of a composition:

$$\{x/f(w,y)\}\{w/a, y/b, z/c\} = \{x/f(a,b), w/a, y/b, z/c\}$$

Now for a key definition.

Definition 4.6 (Definition of Unifiability)   Where an expression is a term or formula, a set $\{\phi_1, \ldots, \phi_n\}$ of expressions is unifiable iff there is a substitution $\sigma$ such that $\phi_1\sigma = \cdots = \phi_n\sigma$. In this case $\sigma$ is said to be a unifier for the set $\{\phi_1, \ldots, \phi_n\}$.

To see Definition 4.6 in action, observe that the substitution $\tau = \{x/a, y/b, z/c\}$ unifies the set

{R(a,y,z), R(x,b,z)}

to produce R(a,b,c). But $\tau$ is not the only unifier of this set. We could have left the variable z unchanged in these two formulas, or we could have substituted some other term for z in both formulas. The important point here is that some substitutions are more general than others. For example, the substitution {x/f(y)} is more general than {x/f(c)}. We say that a subsitution $\sigma$ is as general as or more general than a substitution $\tau$ iff there is another subsitution $\delta$ such that

$$\sigma\delta = \tau.$$

Given this machinery, we can define unifiers with maximum generality:

Definition 4.7 (Definition of Most General Unifier)   Let $\phi$ and $\psi$ be expressions. Then the unifier $\gamma$ is a most general unifier, or mgu, of $\phi$ and $\psi$ provided that, where $\sigma$ is any unifier of these two expressions, there exists a substitution $\delta$ such that

$$\phi\gamma\delta = \phi\sigma = \psi\sigma.$$

For example, the substition {x/a} is an mgu for R(a,y,z) and R(x,y,z).

We can now adapt the resolution principle as defined in Chapter 2 for the propositional case to the first-order case. The basic idea is straightforward. Where $\gamma$ is an mgu for $\phi$ and $\psi$ we have:

$$\begin{array}{ll} \Phi & \mbox{with } \phi \in \Phi\\ \Psi ... ...})\gamma & \mbox{where } \phi\gamma = \psi\gamma\\ \end{array}$$