Unification

After the recipe above we end up with a set of and-ed clauses, each one of which must be true. Each clause is made up of disjuncts. So we have something like

Clause 1 Pred1(ding) Pred2(dong) Pred3(bell)
Clause 2 Pred4(ping) Pred5(pong)
Clause 3 Pred3(king) Pred4(kong)

Now we need to spot pairs negated pairs like Pred3() and Pred3() - but before we can immediately resolve them we need look carefully at what the arguments inside are to ensure that the statements are really contradictory. For example, consider

elephant(Nelly)
elephant(Nelly)
which are obviously contradictory;
genius(J.S.Bach)
genius(C.P.E.Bach)
which are obviously not contradictory; and
cool(x)
cool(flared-trousers)
which are (less obviously) contradictory. In the last case the contradiction arises because the x is universally quantified, so we have the illogical fashion statement that everything is cool except flared trousers.

What is required is a method for checking terms and substituting for the variables. This match and substitute process is called unification.

The unifier looks for

Predicate(args1) and Predicate(args2)
and then asks whether args1 and args2 are unifiable. Variables can be replaced by

For example, C1 and C2 are unifiable, C1 and C3 are not.

C1: P(f(a),x) Q(x)
C2: P(y,g(b)) R(g(b))
C3: P(g(a),x) R(x)

<<<Previous Next>>>