Four-Minute Guide to Resolution
Spring 2010, David Matuszek

Resolution is a means of proving statements in the predicate calculus.
  1. A literal is either a proposition, such as P, Q, it_is_raining, or a predicate, such as P(x), R(x,y), female(Sally), mother(Sally, x).

  2. A clause is a disjunction ("or") of zero or more literals, some or all of which may be negated. For example: sinks(x) ∨ dissolves(X, water) ∨ ¬denser(X, water).

  3. Basic principle of resolution:

    Given: 

    A ∨ someLiterals

    Conclude: 

    ¬A ∨ someOtherLiterals


    someLiterals ∨ someOtherLiterals
  4. Example:

    Given: 

    broke(Bob) ∨ well-fed(Bob)

    Conclude: 

    ¬broke(Bob) ∨ ¬hungry(Bob)
    well-fed(Bob) ∨ ¬hungry(Bob)
  5. There exists a nine-step algorithm for converting any statement in the predicate calculus into a set of clauses. The most interesting aspects of this algorithm are:
  6. Unification is the process of deciding that two literals are "the same". The rules for unification are:
  7. Resolution depends on unification. For example:

    Given: 

    broke(x) ∨ well-fed(x)

    Conclude: 

    ¬broke(Bob) ∨ ¬hungry(Bob)
    well-fed(Bob) ∨ ¬hungry(Bob)
    where x unifies with Bob

  8. Refutation resolution consists of adding the negation of the clause you want to prove, and trying to get to a contradiction (resolving X with ¬X, yielding NIL, the zero-length clause).

  9. Resolution is complete: anything provable can be proved using only the resolution rule.