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 firstorder 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 t_{i} / v_{i} in the existing substitutions
b.Add t_{i} / v_{i} 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: S_{0} => Here, Ψ_{1} = p(f(a), g(Y)), and Ψ_{2} = p(X, X)
SUBST θ = {f(a) / X}
S_{1} => Ψ_{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))}
S_{0} => { p(b, X, f(g(Z))); p(Z, f(Y), f(Y))}
SUBST θ={b/Z}
S_{1} => { p(b, X, f(g(b))); p(b, f(Y), f(Y))}
SUBST θ={f(Y) /X}
S_{2} => { p(b, f(Y), f(g(b))); p(b, f(Y), f(Y))}
SUBST θ= {g(b) /Y}
S_{2} => { 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))
S_{0} => {p (X, X), p (Z, f(Z))}
SUBST θ= {X/Z}
S_{1} => {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)
S_{0} => {Q(a, g(x, a), f(y)); Q(a, g(f(b), a), x)}
SUBST θ= {f(b)/x}
S_{1} => {Q(a, g(f(b), a), f(y)); Q(a, g(f(b), a), f(b))}
SUBST θ= {b/y}
SUBST θ={f(Y) /X}
S_{2} => { p(b, f(Y), f(g(b))); p(b, f(Y), f(Y))}
S_{1} => {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)
S_{0} => { knows(Richard, x); knows(Richard, John)}
S SUBST θ= {John/x}
S_{1} => { knows(Richard, John); knows(Richard, John)}, Successfully Unified.
Unifier: {John/x}.