**Artificial Intelligence**

**History and Application**

**Types of AI**

**Agents in AI**

**Types of AI Agents**

**Agent Environment**

**Turing Test in AI**

**Search Algorithms**

**Uninformed Search Algorithms**

**Informed Search Algorithms**

**Hill Climbing Algorithm**

**Means Ends Analysis**

**Adversarial Search**

**Mini-Max Algorithm**

**Alpha-Beta Pruning**

**Knowledge-based Agent**

**Knowledge Representation**

**Knowledge Representation Techniques**

**Propositional Logic**

**Rules of Inference**

**The Wumpus World**

**Knowledge Base for Wumpus World**

**First Order Logic**

**Knowledge Engineering in FOL**

**Inference in FOL**

**Unification in FOL**

**Resolution in FOL**

**Forward and Backward Chaining**

**Reasoning in AI**

**Bayesian Belief Network**

# 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**Ψ**, then_{1𝜎}= Ψ_{2𝜎}**UNIFY(Ψ**can be written._{1}, Ψ_{2}) **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 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}.**