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.

AI Resolution in First Order Logic in Artificial intelligence (AI)

Where li and 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:

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

To better comprehend all of the preceding phases, we shall use resolution as an example.

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.

AI Resolution in First Order Logic2 in Artificial intelligence (AI)

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:
    1. ∀x ¬ food(x) V likes(John, x)
    2. food(Apple) Λ food(vegetables)
    3. ∀x ∀y ¬ [eats(x, y) Λ ¬ killed(x)] V food(y)
    4. eats (Anil, Peanuts) Λ alive(Anil)
    5. ∀x ¬ eats(Anil, x) V eats(Harry, x)
    6. ∀x¬ [¬ killed(x) ] V alive(x)
    7. ∀x ¬ alive(x) V ¬ killed(x)
    8. likes(John, Peanuts).
  • Move negation (¬)inwards and rewrite
    1. ∀x ¬ food(x) V likes(John, x)
    2. food(Apple) Λ food(vegetables)
    3. ∀x ∀y ¬ eats(x, y) V killed(x) V food(y)
    4. eats (Anil, Peanuts) Λ alive(Anil)
    5. ∀x ¬ eats(Anil, x) V eats(Harry, x)
    6. ∀x ¬killed(x) ] V alive(x)
    7. ∀x ¬ alive(x) V ¬ killed(x)
    8. likes(John, Peanuts).
  • Rename variables or standardize variables
    1. ∀x ¬ food(x) V likes(John, x)
    2. food(Apple) Λ food(vegetables)
    3. ∀y ∀z ¬ eats(y, z) V killed(y) V food(z)
    4. eats (Anil, Peanuts) Λ alive(Anil)
    5. ∀x ¬ eats(Anil, x) V eats(Harry, x)
    6. ∀x ¬killed(x) ] V alive(x)
    7. ∀x ¬ alive(x) V ¬ killed(x)
    8. 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
    1. ¬ food(x) V likes(John, x)
    2. food(Apple)
    3. food(vegetables)
    4. ¬ eats(y, z) V killed(y) V food(z)
    5. eats (Anil, Peanuts)
    6. alive(Anil)
    7. ¬ eats(Anil, w) V eats(Harry, w)
    8. killed(g) V alive(g)
    9. ¬ alive(k) V ¬ killed(k)
    10. 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)

AI Resolution in First Order Logic3 in Artificial intelligence (AI)
As a result, the conclusion's negation has been demonstrated to constitute a total contradiction with the given collection of truths.

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