Artificial Intelligence: Resolution in First Order Logic

In Artificial Intelligence, resolution is a powerful rule of inference used in First-Order Logic (FOL) to prove the validity of logical statements or to derive new conclusions from a set of premises. It is widely used in automated theorem proving, logic programming (e.g., Prolog), and AI reasoning systems. Resolution is particularly effective because it is a complete and sound method for determining whether a set of FOL sentences entails another sentence.

Below, I'll explain resolution in First-Order Logic step-by-step, focusing on its key concepts, process, and application in AI.


1. Overview of Resolution in First-Order Logic

Resolution is a refutation-based proof technique. It works by assuming the negation of the statement to be proven and showing that this leads to a contradiction (i.e., an empty clause). If a contradiction is derived, the original statement must be true (this is called proof by contradiction).

In FOL, resolution operates on clauses, which are disjunctions of literals (a literal is an atomic formula or its negation). The process involves converting FOL sentences into a standardized form (Conjunctive Normal Form, or CNF) and then applying the resolution rule iteratively to derive new clauses until either a contradiction is found or no further progress can be made.


2. Key Concepts

a) First-Order Logic Basics
  • Syntax: FOL consists of constants, variables, predicates, functions, connectives (∧, ∨, ¬, →, ↔), and quantifiers (∀, ∃).
  • Atomic formula: A predicate applied to terms, e.g., P(x, y) or Q(a).
  • Literal: An atomic formula (P(x)) or its negation (¬P(x)).
  • Clause: A disjunction of literals, e.g., P(x) ∨ ¬Q(y) ∨ R(z).
b) Conjunctive Normal Form (CNF)

To apply resolution, all FOL sentences must be converted to CNF, where a formula is a conjunction of clauses. Each clause is a disjunction of literals. For example:

  • (P ∨ Q) ∧ (¬P ∨ R) ∧ (¬Q ∨ ¬R) is in CNF.
  • Steps to convert a formula to CNF:
    1. Eliminate biconditionals (↔) and implications (→) using logical equivalences.
    2. Move negations inward using De Morgan’s laws.
    3. Skolemize to eliminate existential quantifiers (∃) by introducing Skolem constants or functions.
    4. Distribute disjunctions (∨) over conjunctions (∧) to form clauses.
    5. Standardize variables to ensure unique variable names across clauses.
c) Unification

In FOL, resolution requires unification to make literals in two clauses compatible for resolution. Unification finds a substitution of terms for variables that makes two literals identical. For example:

  • To resolve P(x, f(a)) and ¬P(b, y), unify x = b and y = f(a).
  • A most general unifier (MGU) is used to ensure the substitution is as general as possible.
d) Resolution Rule

The resolution rule in FOL is:

  • Given two clauses: C1 = L ∨ A and C2 = ¬L' ∨ B, where L and L' can be unified with substitution θ.
  • Apply the substitution θ to both clauses, then derive a new clause: (A ∨ B)θ.
  • Example:
    • Clauses: P(x) ∨ Q(x) and ¬P(a) ∨ R(a).
    • Unify P(x) and P(a) with θ = {x/a}.
    • Resolve to produce: Q(a) ∨ R(a).


3. Steps for Resolution in FOL

  1. Convert to CNF:
    • Transform all premises and the negation of the conclusion into CNF.
    • Example: To prove ∀x (P(x) → Q(x)) ⊢ Q(a), negate the conclusion (¬Q(a)) and convert all to CNF.
  2. Standardize Variables:
    • Ensure variables in different clauses are distinct to avoid conflicts during unification.
  3. Unify and Resolve:
    • Select two clauses with complementary literals (e.g., P and ¬P).
    • Find the MGU to unify the literals.
    • Apply the resolution rule to derive a new clause.
    • Repeat until:
      • The empty clause ({}) is derived, indicating a contradiction (proof succeeds).
      • No further resolutions are possible (proof fails or is inconclusive).
  4. Check for Contradiction:
    • If the empty clause is derived, the original set of premises entails the conclusion.


4. Example of Resolution in FOL

Problem: Prove ∀x (P(x) → Q(x)), P(a) ⊢ Q(a).

  1. Convert to CNF:
    • Premise 1: ∀x (P(x) → Q(x)) ≡ ∀x (¬P(x) ∨ Q(x)).
      • CNF: ¬P(x) ∨ Q(x).
    • Premise 2: P(a).
      • Already in CNF: P(a).
    • Negation of conclusion: ¬Q(a).
      • CNF: ¬Q(a).

    Clauses:

    • Clause 1: ¬P(x) ∨ Q(x)
    • Clause 2: P(a)
    • Clause 3: ¬Q(a)
  2. Resolution Steps:
    • Resolve Clause 1 (¬P(x) ∨ Q(x)) and Clause 2 (P(a)):
      • Unify P(x) and P(a) with θ = {x/a}.
      • Result: Q(a) (after applying θ to Q(x)).
    • Resolve Q(a) and Clause 3 (¬Q(a)):
      • Complementary literals: Q(a) and ¬Q(a).
      • Result: Empty clause {}.
  3. Conclusion:
    • The empty clause indicates a contradiction, so Q(a) is entailed.


5. Resolution in AI

In AI, resolution is used in:

  • Automated Theorem Proving: To prove theorems or verify properties of systems.
  • Logic Programming: Languages like Prolog use resolution to answer queries.
  • Knowledge-Based Systems: To derive new knowledge from a knowledge base.
  • Planning and Reasoning: To deduce actions or conclusions in intelligent agents.
Advantages:
  • Sound and Complete: Resolution will find a proof if one exists (for FOL, it’s complete for refutation).
  • General-Purpose: Works for any FOL sentence.
  • Automated: Can be implemented efficiently in AI systems.
Challenges:
  • Complexity: Resolution can be computationally expensive due to the need for unification and clause selection.
  • Unification: Finding the MGU can be complex, especially with large knowledge bases.
  • Skolemization: Handling existential quantifiers requires careful introduction of Skolem functions.


6. Practical Considerations

  • Clause Selection Strategies: To improve efficiency, AI systems use strategies like unit preference (preferring clauses with one literal) or set of support (focusing on clauses related to the negated goal).
  • Unification Algorithm: A robust unification algorithm is critical for matching literals.
  • Implementation: Resolution is implemented in systems like Prolog, Otter, or modern theorem provers like Vampire.


7. Example with a Knowledge Base

Knowledge Base:
  • ∀x (Human(x) → Mortal(x)) (All humans are mortal).
  • Human(Socrates) (Socrates is human).

Goal: Prove Mortal(Socrates).

  1. CNF Conversion:
    • ∀x (Human(x) → Mortal(x)) → ¬Human(x) ∨ Mortal(x).
    • Human(Socrates) → Human(Socrates).
    • Negation of goal: ¬Mortal(Socrates).

    Clauses:

    • Clause 1: ¬Human(x) ∨ Mortal(x)
    • Clause 2: Human(Socrates)
    • Clause 3: ¬Mortal(Socrates)
  2. Resolution:
    • Resolve Clause 1 and Clause 2:
      • Unify Human(x) and Human(Socrates) with θ = {x/Socrates}.
      • Result: Mortal(Socrates).
    • Resolve Mortal(Socrates) and Clause 3 (¬Mortal(Socrates)):
      • Result: Empty clause {}.
  3. Conclusion: Mortal(Socrates) is true.


8. Additional Notes

  • Soundness: Resolution only derives clauses that are logically entailed by the premises.
  • Completeness: If a conclusion is entailed, resolution will eventually derive the empty clause.
  • Limitations: Resolution may not terminate for undecidable problems in FOL, and it can be inefficient without optimization.