**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**

# Resolution in FOL in Artificial intelligence

**In this page we will learn about What is Resolution in FOL? in Artificial intelligence,
Resolution in FOL, The resolution inference rule, Steps for Resolution, Explanation of Resolution graph.**

## What is Resolution in FOL?

Resolution is a method of theorem proof that involves constructing refutation proofs, or proofs by contradictions. It was created in 1965 by a mathematician named John Alan Robinson.

When several statements are supplied and we need to prove a conclusion from those claims, we employ resolution. In proofs by resolutions, unification is a crucial idea. Resolution is a single inference rule that can work on either the **conjunctive normal form or the clausal form efficiently.**
**Clause:** A clause is a disjunction of literals (an atomic sentence). It's sometimes referred to as a unit clause.
**Conjunctive Normal Form (CNF):** Conjunctive normal form (CNF) is a sentence that is represented as a conjunction of clauses.
**Note: Firstly learn the FOL in AI, to better understand this topic. **

### The resolution inference rule:

The propositional rule is just a lifted version of the resolution rule for first-order logic. If two clauses include complementary literals that are expected to be standardized apart so that they share no variables, resolution can resolve them.

Where

**l**and

_{i}**mj**are complementary literals, there is a resolution in FOL.

Because it only resolves perfectly, this rule is also known as the

**binary resolution rule**.

**Example:**

We can determine two clauses which are given below:

**[Animal (g(x) V Loves (f(x), x)] and [￢ Loves(a, b) V ￢Kills(a, b)]**

**Two complimentary literals are: Loves (f(x), x) and ￢ Loves (a, b)**

These literals could be unified with

**unifier θ= [a/f(x), and b/x]**, and it will bring about a resolvent clause:

**[Animal (g(x) V ￢ Kills(f(x), x)].**

### Steps for Resolution:

- Conversion of facts into first-order logic
- Convert FOL statements into CNF
- Negate the statement which needs to prove (proof by contradiction)
- Draw resolution graph (unification)

### Example:

**Anything anyone eats and not killed is food.****Anil eats peanuts and still alive****Harry eats everything that Anil eats.****John likes all kind of food.****Apple and vegetable are food****Prove by resolution that:****John likes peanuts.**

### Step-1: Conversion of Facts into FOL

We'll start by converting all of the given propositions to first-order logic.

### Step-2: Conversion of FOL into CNF

Converting FOL to CNF is essential in first-order logic resolution because CNF makes resolution proofs easier.

**Eliminate all implication (→) and rewrite**- ∀x ¬ food(x) V likes(John, x)
- food(Apple) Λ food(vegetables)
- ∀x ∀y ¬ [eats(x, y) Λ ¬ killed(x)] V food(y)
- eats (Anil, Peanuts) Λ alive(Anil)
- ∀x ¬ eats(Anil, x) V eats(Harry, x)
- ∀x¬ [¬ killed(x) ] V alive(x)
- ∀x ¬ alive(x) V ¬ killed(x)
- likes(John, Peanuts).

**Move negation (¬)inwards and rewrite**- ∀x ¬ food(x) V likes(John, x)
- food(Apple) Λ food(vegetables)
- ∀x ∀y ¬ eats(x, y) V killed(x) V food(y)
- eats (Anil, Peanuts) Λ alive(Anil)
- ∀x ¬ eats(Anil, x) V eats(Harry, x)
- ∀x ¬killed(x) ] V alive(x)
- ∀x ¬ alive(x) V ¬ killed(x)
- likes(John, Peanuts).

**Rename variables or standardize variables**- ∀x ¬ food(x) V likes(John, x)
- food(Apple) Λ food(vegetables)
- ∀y ∀z ¬ eats(y, z) V killed(y) V food(z)
- eats (Anil, Peanuts) Λ alive(Anil)
- ∀x ¬ eats(Anil, x) V eats(Harry, x)
- ∀x ¬killed(x) ] V alive(x)
- ∀x ¬ alive(x) V ¬ killed(x)
- likes(John, Peanuts).

**Eliminate existential instantiation quantifier by elimination.**

We will eliminate existential quantifiers in this step, which is referred to as**Skolemization**. However, because there is no existential quantifier in this example problem, all of the assertions in this phase will be the same**Drop Universal quantifiers.**We'll remove all universal quantifiers ∃ in this phase because none of the statements are implicitly quantified, therefore we don't need them- ¬ food(x) V likes(John, x)
- food(Apple)
- food(vegetables)
- ¬ eats(y, z) V killed(y) V food(z)
- eats (Anil, Peanuts)
- alive(Anil)
- ¬ eats(Anil, w) V eats(Harry, w)
- killed(g) V alive(g)
- ¬ alive(k) V ¬ killed(k)
- likes(John, Peanuts).

**[ Note: Statements "food(Apple) Λ food(vegetables)" and "eats (Anil, Peanuts) Λ alive(Anil)" can be written in two independent statements. ]**

**Distribute conjunction ∧ over disjunction ¬.**This step will not make any change in this problem.

### Step 3: Reverse the statement that needs to be proven.

We will use negation to write the conclusion assertions in this statement, which will be written as "likes" (John, Peanuts)

### Step 4: Create a graph of resolution:

In this stage, we'll use a resolution tree and substitution to solve the problem. It will be as follows for the aforesaid problem:

### Explanation of Resolution graph:

- First step:
**¬likes(John, Peanuts)**, and**likes(John, x)**get resolved(canceled) by substitution of {Peanuts/x}, and we are left with**¬ food(Peanuts)** - Second step:
**¬ food(Peanuts)**, and**food(z)**get resolved (canceled) by substitution of**{ Peanuts/z}**, and we are left with**¬ eats(y, Peanuts) V killed(y)**. - Third step:
**¬ eats(y, Peanuts)**and**eats (Anil, Peanuts)**get resolved by substitution**{Anil/y}**, and we are left with**Killed(Anil)**. - Fourth step:
**Killed(Anil)**and**¬ killed(k)**get resolve by substitution**{Anil/k}**, and we are left with**¬ alive(Anil)**. - Last step:
**¬ alive(Anil)**and**alive(Anil)**get resolve