Four-Minute Guide to Resolution
Spring 2010, David Matuszek

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.