Four-Minute Guide to Resolution
Fall 2015, 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:
• 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.