Fall 2015, David Matuszek

Resolution is a means of proving statements in the predicate calculus.

- 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)`

.

- 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)`

.

**Basic principle of resolution:**Given:

`A ∨ someLiterals`

Conclude:

`¬A ∨ someOtherLiterals`

`someLiterals ∨ someOtherLiterals`

- Example:
Given:

`broke(Bob) ∨ well-fed(Bob)`

Conclude:

`¬broke(Bob) ∨ ¬hungry(Bob)`

`well-fed(Bob) ∨ ¬hungry(Bob)`

- 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
(∀).

- Existentially quantified (∃) variables become
*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.

- 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`

*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).

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