Unification First Order Logic

What is Unification in Artificial intelligence?

In this page we will learn about Unification in Artificial intelligence, What is Unification in Artificial intelligence, Conditions for Unification, Unification Algorithm, Implementation of the Algorithm.

What is Unification?

  • Unification is the process of finding a substitute that makes two separate logical atomic expressions identical. The substitution process is necessary for unification.
  • It accepts two literals as input and uses substitution to make them identical.
  • Let Ψ1 and Ψ2 be two atomic sentences, and be a unifier such that Ψ1𝜎 = Ψ2𝜎, then UNIFY(Ψ1, Ψ2)can be written.
  • Example: Find the MGU for Unify{King(x), King(John)}
     Let Ψ1 = King(x), Ψ2 = King(John),

Substitution θ = {John/x} is a unifier for these atoms, and both equations will be equivalent if this substitution is used.

  • For unification, the UNIFY algorithm is employed, which takes two atomic statements and returns a unifier for each of them (If any exist).
  • All first-order inference techniques rely heavily on unification.
  • If the expressions do not match, the result is failure.
  • The replacement variables are referred to as MGU (Most General Unifier).

    • E.g. Let's say there are two different expressions, P(x, y), and P(a, f(z)).
      In this case, we must make both of the preceding assertions identical. For this, we'll make a substitute.
      P(x, y)......... (i)
      P(a, f(z))......... (ii)
      Substitute x with a, and y with f(z) in the first expression, and it will be represented as a/x and f(z)/y.
      The first expression will be identical to the second expression with both replacements, and the substitution set will be: [a/x , f(z)/y].

Conditions for Unification

The following are some fundamental requirements for unification:

  • Atoms or expressions with various predicate symbols can never be united.
  • Both phrases must have the same number of arguments.
  • If two comparable variables appear in the same expression, unification will fail.

Unification Algorithm:

Algorithm: Unify(Ψ1, Ψ2)


  Step. 1: If Ψ1 or Ψ2 is a variable or constant, then: 
       a) If Ψ1 or Ψ2 are identical, then return NIL. 
       b) Else if Ψ1 is a variable, 
               a. then if Ψ1 occurs in Ψ2, then return FAILURE
               b. Else return { (Ψ2/ Ψ1)}.
       c) Else if Ψ2 is a variable, 
               a. If Ψ2 occurs in Ψ1 then return FAILURE,
               b. Else return {( Ψ1 / Ψ2)}. 
       d) Else return FAILURE. 
  Step.2: If the initial Predicate symbol in Ψ1 and Ψ2 are not same, then return FAILURE.
  Step. 3: IF Ψ1 and Ψ2 have a different number of arguments, then return FAILURE.
  Step. 4: Set Substitution set(SUBST) to NIL. 
  Step. 5: For i=1 to the number of elements in Ψ1. 
        a) Call Unify function with the ith element of Ψ1 and ith element of Ψ2, and put the result into S.
        b) If S = failure then returns Failure
        c) If S ≠ NIL then do,
                a. Apply S to the remainder of both L1 and L2.
                b. SUBST= APPEND(S, SUBST). 
  Step.6: Return SUBST.

Implementation of the Algorithm

Step 1: Begin by making the substitute set empty.
Step 2: Unify atomic sentences in a recursive manner:
   a.Check for expressions that are identical.
   b.If one expression is a variable vΨi, and the other is a term ti which does not contain variable vi, then:
      a. Substitute ti / vi in the existing substitutions
       b.Add ti / vi to the substitution setlist.
      c. If both the expressions are functions, then function name must be similar, and the number of       arguments must be the same in both the expression.
Find the most general unifier for each pair of the following atomic statements (If exist).

1. Find the MGU of {p(f(a), g(Y)) and p(X, X)}

   Sol: S0 => Here, Ψ1 = p(f(a), g(Y)), and Ψ2 = p(X, X)
    SUBST θ = {f(a) / X}
     S1 => Ψ1 = p(f(a), g(Y)), and Ψ2 = p(f(a), f(a))
    SUBST θ = {f(a) / g(y)}, Unification failed.
Unification is not possible for these expressions.

2. Find the MGU of {p(b, X, f(g(Z))) and p(Z, f(Y), f(Y))}

S0 => { p(b, X, f(g(Z))); p(Z, f(Y), f(Y))}
SUBST θ={b/Z}

S1 => { p(b, X, f(g(b))); p(b, f(Y), f(Y))}
SUBST θ={f(Y) /X}

S2 => { p(b, f(Y), f(g(b))); p(b, f(Y), f(Y))}
SUBST θ= {g(b) /Y}

S2 => { p(b, f(g(b)), f(g(b)); p(b, f(g(b)), f(g(b))} Unified Successfully.
And Unifier = { b/Z, f(Y) /X , g(b) /Y}.

3. Find the MGU of {p (X, X), and p (Z, f(Z))}

Here, Ψ1 = {p (X, X), and Ψ2 = p (Z, f(Z))
S0 => {p (X, X), p (Z, f(Z))}
SUBST θ= {X/Z}
    S1 => {p (Z, Z), p (Z, f(Z))}
SUBST θ= {f(Z) / Z}, Unification Failed.
Therefore, unification is not possible for these expressions.

5. Find the MGU of Q(a, g(x, a), f(y)), Q(a, g(f(b), a), x)}

Here, Ψ1 = Q(a, g(x, a), f(y)), and Ψ2 = Q(a, g(f(b), a), x)
S0 => {Q(a, g(x, a), f(y)); Q(a, g(f(b), a), x)}
SUBST θ= {f(b)/x}
S1 => {Q(a, g(f(b), a), f(y)); Q(a, g(f(b), a), f(b))}

SUBST θ= {b/y}
SUBST θ={f(Y) /X}

S2 => { p(b, f(Y), f(g(b))); p(b, f(Y), f(Y))}
S1 => {Q(a, g(f(b), a), f(b)); Q(a, g(f(b), a), f(b))}, Successfully Unified.
Unifier: [a/a, f(b)/x, b/y].

6. UNIFY(knows(Richard, x), knows(Richard, John))

Here, Ψ1 = knows(Richard, x), and Ψ2 = knows(Richard, John)
S0 => { knows(Richard, x); knows(Richard, John)}
S SUBST θ= {John/x}
S1 => { knows(Richard, John); knows(Richard, John)}, Successfully Unified.
Unifier: {John/x}.