Unification

• Given two substitutions S = [t1/x1 .. tn/xn] and V = [u1/y1 .. um/ym], the composition of S and V, S . V, is the substitution obtained by,

o Applying V to t1 .. tn [the operation on substitutions with just this property is called concatenation], and adding any pair uj/yj such that yj is not in {x1 .. xn}.

For example: [G(x y)/z].[A/x B/y C/w D/z] is [G(A B)/z A/x B/y C/w].

Composition is an operation that is associative and non commutative

• A set of forms f1 .. fn is unifiable iff there is a substitution S such that f1.S = f2.S= .. = fn.S. We then say that S is a unifier of the set.

For example {P(x F(y) B) P(x F(B) B)} is unified by [A/x B/y] and also unifiedby [B/y].

• A Most General Unifier (MGU) of a set of forms f1 .. fn is a substitution S that unifies this set and such that for any other substitution T that unifies the set there is a substitution V such that S.V = T. The result of applying the MGU to the forms is called a Most General Instance (MGI). Here are some examples:

Resolution

We have introduced the inference rule Modus Ponens. Now we introduce another

inference rule that is particularly significant, Resolution. Since it is not trivial to understand, we proceed in two steps. First we introduce Resolution in the Propositional Calculus, that is, in a language with only truth valued variables. Then we generalize to First Order Logic.

Resolution in the Propositional Calculus

In its simplest form Resolution is the inference rule:

{A OR C, B OR (NOT C)}

----------------------

A OR B

More in general the Resolution Inference Rule is:

• Given as premises the clauses C1 and C2, where C1 contains the literal L and C2

contains the literal (NOT L), infer the clause C, called the Resolvent of C1 and

C2, where C is the union of (C1 - {L}) and (C2 -{(NOT L)})

In symbols:

{C1, C2}

---------------------------------

(C1 - {L}) UNION (C2 - {(NOT L)})

Example:

The following set of clauses is inconsistent:

1. (P OR (NOT Q))

2. ((NOT P) OR (NOT S))

3. (S OR (NOT Q))

4. Q

In fact:

5. ((NOT Q) OR (NOT S)) from 1. and 2.

6. (NOT Q) from 3. and 5.

7. FALSE from 4. and 6.

Notice that 7. is really the empty clause.

Theorem: The Propositional Calculus with the Resolution Inference Rule is sound

and Refutation Complete.

 This theorem requires that clauses be represented as sets, that is, that each

element of the clause appear exactly once in the clause. This requires some form of

membership test when elements are added to a clause.

C1 = {P P}

C2 = {(NOT P) (NOT P)}

C = {P (NOT P)}

From now on by resolution we just get again C1, or C2, or C.