What is Unification?

• Unification is a process of making two different logical atomic expressions identical by finding a substitution. Unification depends on the substitution process.
• It takes two literals as input and makes them identical using substitution.
• Let Ψ₁ and Ψ₂ be two atomic sentences and ? be a unifier such that, Ψ₁? = Ψ₂?, then it can be expressed as UNIFY(Ψ₁, Ψ₂).
• Example: Find the MGU for Unify{King(x), King(John)}

Let Ψ₁ = King(x), Ψ₂ = King(John),

Substitution θ = {John/x} is a unifier for these atoms and applying this substitution, and both expressions will be identical.

• The UNIFY algorithm is used for unification, which takes two atomic sentences and returns a unifier for those sentences (If any exist).
• Unification is a key component of all first-order inference algorithms.
• It returns fail if the expressions do not match with each other.
• The substitution variables are called Most General Unifier or MGU.

E.g. Let's say there are two different expressions, P(x, y), and P(a, f(z)).

In this example, we need to make both above statements identical to each other. For this, we will perform the substitution.

            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.
• With both the substitutions, the first expression will be identical to the second expression and the substitution set will be: [a/x, f(z)/y].

Conditions for Unification:

Following are some basic conditions for unification:

• Predicate symbol must be same, atoms or expression with different predicate symbol can never be unified.
• Number of Arguments in both expressions must be identical.
• Unification will fail if there are two similar variables present in the same expression.

Unification Algorithm:

Algorithm: Unify(Ψ₁, Ψ₂)

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 Ψ1is 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: Initialize the substitution set to be empty.

Step.2: Recursively unify atomic sentences:

1. Check for Identical expression match.
2. If one expression is a variable v_i, and the other is a term t_i which does not contain variable v_i, then:
   1. Substitute t_i / v_i in the existing substitutions
   2. Add t_i /v_i to the substitution setlist.
   3. 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.

For each pair of the following atomic sentences find the most general unifier (If exist).

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

            Sol: S₀ => Here, Ψ₁ = p(f(a), g(Y)), and Ψ₂ = p(X, X)
                  SUBST θ= {f(a) / X}
                  S1 => Ψ₁ = p(f(a), g(Y)), and Ψ₂ = 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))}

Here, Ψ₁ = p(b, X, f(g(Z))) , and Ψ₂ = p(Z, f(Y), f(Y))
S₀ => { p(b, X, f(g(Z))); p(Z, f(Y), f(Y))}
SUBST θ={b/Z}

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

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

S₂ => { 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, Ψ₁ = {p (X, X), and Ψ₂ = p (Z, f(Z))
S₀ => {p (X, X), p (Z, f(Z))}
SUBST θ= {X/Z}
              S1 => {p (Z, Z), p (Z, f(Z))}
SUBST θ= {f(Z) / Z}, Unification Failed.

Hence, unification is not possible for these expressions.

4. Find the MGU of UNIFY(prime (11), prime(y))

Here, Ψ₁ = {prime(11) , and Ψ₂ = prime(y)}
S₀ => {prime(11) , prime(y)}
SUBST θ= {11/y}

S₁ => {prime(11) , prime(11)} , Successfully unified.
              Unifier: {11/y}.

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

Here, Ψ₁ = Q(a, g(x, a), f(y)), and Ψ₂ = Q(a, g(f(b), a), x)
S₀ => {Q(a, g(x, a), f(y)); Q(a, g(f(b), a), x)}
SUBST θ= {f(b)/x}
S₁ => {Q(a, g(f(b), a), f(y)); Q(a, g(f(b), a), f(b))}

SUBST θ= {b/y}
S₁ => {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, Ψ₁ = knows(Richard, x), and Ψ₂ = knows(Richard, John)
S₀ => { knows(Richard, x); knows(Richard, John)}
SUBST θ= {John/x}
S₁ => { knows(Richard, John); knows(Richard, John)}, Successfully Unified.
Unifier: {John/x}.