CSC 8520-001: Four-Minute Guide to Resolution
Wednesdays from 6:15pm to 8:45pm in Mendel G29
Dr. David Matuszek, Mendel 162C, (610) 519-5654
Villanova University, Spring 2000

  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:
    • Existentially quantified () variables become Skolem constants or Skolem functions.
    • All remaining variables are assumed to be universally quantified ().

  6. Unification is the process of deciding that two literals are "the same". The rules for unification are:
    • A variable can be unified with anything.
    • Two constants can be unified only if they are identical.
    • Two predicates can be unified if and only if their respective arguments can be unified.

  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.