Resolution in First-Order Logic (FOL)

Table of Content:

Content Highlight:

Resolution is a powerful theorem-proving technique invented by mathematician John Alan Robinson in 1965. It establishes the truth of a statement by building refutation proofs using unification to combine statements and resolve them in conjunctive normal form (CNF). In First-Order Logic (FOL), resolution involves converting statements to CNF, applying unification, and resolving clauses until the empty clause is derived. For example, to prove P → R from P → Q and Q → R, we convert to CNF, negate the conclusion, and resolve step-by-step. The resolution rule in FOL resolves two clauses with complementary literals. For instance, Loves(f(x), x) and ¬Loves(a, b) can be unified to generate Animal(g(x)) ∨ ¬Kills(f(x), x). This method is particularly useful in fields like artificial intelligence and formal verification. To prove that John likes peanuts, we convert facts to FOL statements, transform them to CNF, negate the statement, and resolve step-by-step until a contradiction is found, proving the original statement true.

What is Resolution in First-Order Logic (FOL)?

Resolution is a theorem-proving technique used to establish the truth of a statement by building refutation proofs, or proofs by contradiction. This method was invented by mathematician John Alan Robinson in 1965.

How Resolution Works?

When multiple statements are given, and a conclusion needs to be proven from those statements, resolution can be used. A key aspect of this process is unification, which is crucial for combining statements to reach a conclusion. Resolution operates efficiently on statements in conjunctive normal form (CNF) or clausal form.

Key Concepts of resulation:

Clause: A clause is a disjunction of literals (atomic sentences). It's also known as a unit clause if it contains only one literal.

Conjunctive Normal Form (CNF): A sentence is in CNF if it is a conjunction of clauses.

Resolution in First-Order Logic:

In First-Order Logic (FOL), resolution involves the following steps:

  1. Convert to CNF: Transform all given statements and the negation of the conclusion into CNF.
  2. Apply Unification: Use unification to match literals from different clauses, combining them where possible.
  3. Resolve: Apply the resolution rule to generate new clauses. This involves finding pairs of clauses that contain complementary literals (e.g., P and ¬P) and resolving them to produce a new clause.
  4. Repeat: Continue resolving clauses until either the empty clause is derived, indicating a contradiction, or no further resolution is possible.

Example:

Given statements:

  1. P → Q
  2. Q → R

And we want to prove P → R.

Convert to CNF:

  1. ¬P ∨ Q
  2. ¬Q ∨ R

Negate the conclusion and convert to CNF:

  1. P
  2. ¬R

Combine and resolve:

  1. From ¬P ∨ Q and P, we get Q.
  2. From ¬Q ∨ R and Q, we get R.
  3. From R and ¬R, we get the empty clause.

Since we derived the empty clause, the original conclusion P → R is proven by contradiction.

Resolution in FOL is a powerful method for automated theorem proving, particularly in fields like artificial intelligence and formal verification.

Resolution rules in First-Order Logic (FOL):

The resolution inference rule for first-order logic is an extension of the propositional resolution rule. It operates by resolving two clauses that contain complementary literals. These literals are standardized apart to ensure they share no variables.

The rule can be visualized as:


l1 ∨ ... ∨ lk,    m1 ∨ ... ∨ mn
SUBST(θ, l1 ∨ ... ∨ li-1 ∨ li+1 ∨ ... ∨ lk ∨ m1 ∨ ... ∨ mj-1 ∨ mj+1 ∨ ... ∨ mn)

Where li and mj are complementary literals, and θ is the unifier that makes them complementary.

This rule is often referred to as the binary resolution rule because it resolves exactly two literals.

Example:

Consider the following clauses:

  1. [ Animal(g(x)) ∨ Loves(f(x), x) ]
  2. [ ¬Loves(a, b) ∨ ¬Kills(a, b) ]

Here, the complementary literals are Loves(f(x), x) and ¬Loves(a, b).

Using the unifier θ = [a/f(x), b/x], we can unify these literals and generate the resolvent clause:

[ Animal(g(x)) ∨ ¬Kills(f(x), x) ]

Explanation:

  1. Identify Complementary Literals: Look for literals in the two clauses that can be made complementary through unification.
  2. Apply Unification: Use a unifier to make the complementary literals identical.
  3. Generate Resolvent Clause: Substitute the unified literals into the remaining parts of the clauses to produce the new clause.

Example Scenario:

Given the following facts:

  1. John likes all kinds of food.
  2. Apples and vegetables are food.
  3. Anything anyone eats and isn't killed by is food.
  4. Anil eats peanuts and is still alive.
  5. Harry eats everything that Anil eats.

We need to prove by resolution that: John likes peanuts.

Step-by-Step Process:-

Step 1: Convert Facts into First-Order Logic (FOL) Statements:

  1. John likes all kinds of food: ∀x (Food(x) → Likes(John, x))
  2. Apples and vegetables are food: Food(Apple) and Food(Vegetable)
  3. Anything anyone eats and isn't killed by is food: ∀x ∀y (Eats(x, y) ∧ ¬Killed(x, y) → Food(y))
  4. Anil eats peanuts and is still alive: Eats(Anil, Peanut) and ¬Killed(Anil, Peanut)
  5. Harry eats everything that Anil eats: ∀x (Eats(Anil, x) → Eats(Harry, x))

Step 2: Convert FOL Statements into CNF:

  1. ∀x (Food(x) → Likes(John, x)) becomes ¬Food(x) ∨ Likes(John, x)
  2. Food(Apple) (already in CNF)
  3. Food(Vegetable) (already in CNF)
  4. ∀x ∀y (Eats(x, y) ∧ ¬Killed(x, y) → Food(y)) becomes ¬Eats(x, y) ∨ ¬Killed(x, y) ∨ Food(y)
  5. Eats(Anil, Peanut) (already in CNF)
  6. ¬Killed(Anil, Peanut) (already in CNF)
  7. ∀x (Eats(Anil, x) → Eats(Harry, x)) becomes ¬Eats(Anil, x) ∨ Eats(Harry, x)

Step 3: Negate the Statement to be Proven:

Negate the statement "John likes peanuts": ¬Likes(John, Peanut)

Step 4: Draw Resolution Graph and Apply Unification:

Combine all the clauses including the negated statement and resolve them step-by-step:

  1. Start with ¬Likes(John, Peanut)
  2. Use ¬Food(x) ∨ Likes(John, x) with x = Peanut: ¬Food(Peanut) ∨ Likes(John, Peanut)
  3. Resolve with ¬Likes(John, Peanut): Result: ¬Food(Peanut)
  4. Use ¬Eats(x, y) ∨ ¬Killed(x, y) ∨ Food(y) with x = Anil and y = Peanut: ¬Eats(Anil, Peanut) ∨ ¬Killed(Anil, Peanut) ∨ Food(Peanut)
  5. Given Eats(Anil, Peanut) and ¬Killed(Anil, Peanut): Result: Food(Peanut)
  6. Resolve ¬Food(Peanut) and Food(Peanut) to derive a contradiction
Draw Resolution Graph and Apply Unification

Explanation of Resolution graph:

The resolution graph begins with the clause ¬likes(John, Peanuts). In the first step, this clause is resolved with ¬food(x) ∨ likes(John, x) by substituting {Peanuts/x}, resulting in the clause ¬food(Peanuts). In the second step, ¬food(Peanuts) is resolved with ¬eats(y, z) ∨ ¬killed(y) ∨ food(z) using the substitution {Peanuts/z}, which simplifies to ¬eats(y, Peanuts) ∨ killed(y). The third step involves resolving ¬eats(y, Peanuts) with eats(Anil, Peanuts) by substituting {Anil/y}, leading to killed(Anil). In the fourth step, killed(Anil) is resolved with ¬alive(k) ∨ ¬killed(k) using the substitution {Anil/k}, resulting in the clause ¬alive(Anil). Finally, ¬alive(Anil) is resolved with alive(Anil), producing the empty clause {}. This contradiction indicates that the negation of the initial statement is false, thus proving that "John likes peanuts" is true by resolution.

The contradiction proves that the negation of our statement is false. Therefore, the original statement "John likes peanuts" is proven true by resolution.

The resolution rule in FOL is a powerful tool for automated theorem proving, particularly in fields like artificial intelligence and formal verification. It allows for the systematic resolution of clauses, enabling the derivation of new knowledge from existing statements.