
Introduction to Logic

Tools for Thought

What differentiates Resolution from propositional resolution is unification. In propositional resolution, two clauses resolve if they contain complementary literals, i.e. the positive literal is identical to the target of the negative literal. The same idea underlies Resolution, except that the criterion for complementarity is relaxed. The positive literal does not need to be identical to the target of the negative literal; it is sufficient that the two can be made identical by substitutions for their variables.
Unification is the process of determining whether two expressions can be unified, i.e. made identical by appropriate substitutions for their variables. As we shall see, making this determination is an essential part of resolution.

A substitution is a finite mapping of variables to terms. In what follows, we write substitutions as sets of replacement rules, like the one shown below. In each rule, the variable to which the arrow is pointing is to be replaced by the term from which the arrow is pointing. In this case, x is to be replaced by a, y is to be replaced by f(b), and z is to be replaced by v.
{x←a, y←f(b), z←v}
The variables being replaced together constitute the domain of the substitution, and the terms replacing them constitute the range. For example, in the preceding substitution, the domain is {x, y, z}, and the range is {a, f(b), v}.

A substitution is pure if and only if all replacement terms in the range are free of the variables in the domain of the substitution. Otherwise, the substitution is impure. The substitution shown above is pure whereas the one shown below is impure.
{x←a, y←f(b), z←x}

The result of applying a substitution σ to an expression φ is the expression φσ obtained from the original expression by replacing every occurrence of every variable in the domain of the substitution by the term with which it is associated.
q(x, y){x←a, y←f(b), z←v} 
= 
q(a, f(b)) 
q(x, x){x←a, y←f(b), z←v} 
= 
q(a, a) 
q(x, w){x←a, y←f(b), z←v} 
= 
q(a, w) 
q(z, v){x←a, y←f(b), z←v} 
= 
q(v, v) 

Note that, if a substitution is pure, application is idempotent, i.e. applying a substitution a second time has no effect.
q(x, x, y, w, z){x←a, y←f(b), z←v} 
= 
q(a, a, f(b), w, v) 
q(a, a, f(b), w, v){x←a, y←f(b), z←v} 
= 
q(a, a, f(b), w, v) 
However, this is not the case for impure substitutions, as illustrated by the following example. Applying the substitution once leads to an expression with an x, allowing for a different answer when the substitution is applied a second time.
q(x, x, y, w, z){x←a, y←f(b), z←x} 
= 
q(a, a, f(b), w, x) 
q(a, a, f(b), w, x){x←a, y←f(b), z←x} 
= 
q(a, a, f(b), w, a) 

Given two or more substitutions, it is possible to define a single substitution that has the same effect as applying those substitutions in sequence. For example, the substitutions {x←a, y←f(u), z←v} and {u←d, v←e} can be combined to form the single substitution {x←a, y←f(d), z←e, u←d, v←e}, which has the same effect as the first two substitutions when applied to any expression whatsoever.
Computing the composition of a substitution σ and a substitution τ is easy. There are two steps. (1) First, we apply τ to the range of σ. (2) Then we adjoin to σ all pairs from τ with different domain variables.
As an example, consider the composition shown below. In the right hand side of the first equation, we have applied the second substitution to the replacements in the first substitution. In the second equation, we have combined the rules from this new substitution with the nonconflicting rules from the second substitution.
 {x←a, y←f(u), z←v}{u←d, v←e, z←g}
 = {x←a, y←f(d), z←e}{u←d, v←e, z←g}
 = {x←a, y←f(d), z←e, u←d, v←e}

It is noteworthy that composition does not necessarily preserve substitutional purity. The composition of two impure substitutions may be pure, and the composition of two pure substitutions may be impure.
This problem does not occur if the substitutions are composable. A substitution σ and a substitution τ are composable if and only if the domain of σ and the range of τ are disjoint. Otherwise, they are noncomposable.
{x←a, y←b, z←v}{x←u, v←b}
By contrast, the following substitutions are noncomposable. Here, x occurs in both the domain of the first substitution
and the range of the second substitution, violating the definition of composability.
{x←a, y←b, z←v}{x←u, v←x}
The importance of composability is that it ensures preservation of purity. The composition of composable pure substitutions must be pure. In the sequel, we look only at compositions of composable pure substitutions.

A substitution σ is a unifier for an expression φ and an expression ψ if and only if φσ=ψσ, i.e. the result of applying σ to φ is the same as the result of applying σ to ψ. If two expressions have a unifier, they are said to be unifiable. Otherwise, they are nonunifiable.
The expressions p(x, y) and p(a,v) have a unifier, e.g. {x←a, y←b, v←b} and are, therefore, unifiable. The results of applying this substitution to the two expressions are shown below.
p(x, y){x←a, y←b, v←b}=p(a, b)
p(a, v){x←a, y←b, v←b}=p(a, b)
Note that, although this substitution unifies the two expressions, it is not the only unifier. We do not have to substitute b for y and v to unify the two expressions. We can equally well substitute c or d or f(c) or f(w). In fact, we can unify the expressions without changing v at all by simply replacing y by v.

In considering these alternatives, it should be clear that some substitutions are more general than others. We say that a substitution σ is as general as or more general than a substitution τ if and only if there is another substitution δ such that σδ=τ. For example, the substitution {x←a, y←v} is more general than {x←a, y←f(c), v←f(c)} since there is a substitution {v←f(c)} that, when applied to the former, gives the latter.
{x←a, y←v}{v←f(c)}={x←a, y←f(c), v←f(c)}
In resolution, we are interested only in unifiers with maximum generality. A most general unifier, or mgu, σ of two expressions has the property that it as general as or more general than any other unifier.
Although it is possible for two expressions to have more than one most general unifier, all of these most general unifiers are structurally the same, i.e. they are unique up to variable renaming. For example, p(x) and p(y) can be unified by either the substitution {x←y} or the substitution {y←x}; and either of these substitutions can be obtained from the other by applying a third substitution. This is not true of the unifiers mentioned earlier.

One good thing about our language is that there is a simple and inexpensive procedure for computing a most general unifier of any two expressions if it exists.
The procedure assumes a representation of expressions as sequences of subexpressions. For example, the expression p(a, f(b),z) can be thought of as a sequence with four elements, viz. the relation constant p, the object constant a, the term f(b), and the variable z. The term f(b) can in turn be thought of as a sequence of two elements, viz. the function constant f and the object constant b.
We start the procedure with two expressions and a substitution, which is initially the empty substitution. We then recursively process the two expressions, comparing the subexpressions at each point. Along the way, we expand the substitution with variable assignments as described below. If, we fail to unify any pair of subexpression at any point in this process, the procedure as a whole fails. If we finish this recursive comparison of the expressions, the procedure as a whole succeeds, and the accumulated substitution at that point is the most general unifier.

In comparing two subexpressions, we first apply the substitution to each of the two expressions; and we then execute the following procedure on the two modified expressions.
1. If the modified expressions are identical, then nothing more needs to be done, and the procedure succeeds.
2. If the modified expressions are not identical and one is a variable, we check whether the second modified expression is a term containing the variable. If the variable occurs within the expression, we fail; otherwise, we update our substitution to the composition of the old substitution and a new substitution in which we bind the variable to the second modified expression.
3. If the modified expressions are not identical and neither is a variable and at least one is a constant, then we fail, since there is no way to make them look alike.
4. The only remaining possibility is that the two modified expressions are both sequences. In this case, we simply iterate across the expressions, comparing as described above.

As an example, consider the computation of the most general unifier for the expressions p(x,b) and p(a,y) with the initial substitution {}. A trace of the execution of the procedure for this case is shown below. We show the beginning of a comparison with a line labelled Compare together with the expressions being compared and the input substitution. We show the result of each comparison with a line labelled Result. The indentation shows the depth of recursion of the procedure.
Compare: p(x,b), p(a,y), {} 
Compare: p, p, {} 
Result: {} 
Compare: x, a, {} 
Result: {x←a} 
Compare: y, b, {x←a} 
Result: {x←a, y←b} 
Result: {x←a, y←b} 

As another example, consider the process of unifying the expression p(x,x) and the expression p(a,y). A trace is shown below. The main interest in this example comes in comparing the last argument in the two expressions, viz. x and y. By the time we reach this point, x is bound to a, so we replace it by a before comparing. y has no binding so we leave it as is. Finally we compare a and y, which results in a binding of y to a.
Compare: p(x,x), p(a,y), {} 
Compare: p, p, {} 
Result: {} 
Compare: x, a, {} 
Result: {x←a} 
Compare: a, y, {x←a} 
Result: {x←a, y←a} 
Result: {x←a, y←a} 

One especially noteworthy part of the unification procedure is the test for whether a variable occurs within an expression before the variable is bound to that expression. This test is called an occur check since it is used to check whether or not the variable occurs within the term with which it is being unified. Without this check, the algorithm would find that expressions such as p(x) and p(f(x)) are unifiable, even though there is no substitution for x that, when applied to both, makes them look alike.

Use the arrow keys to navigate.
