Resolution Practice Problems
Fall 2011, David Matuszek

Unification is an important aspect of resolution. For each of the following attempted unifications, tell what variable instantiations and unifications result.

  1. foo(X, Y) = foo(a, a)

  2. foo(X, Y) = foo(a, X)

  3. foo(X, Y) = foo(Y, X)

  4. mother(mary, X) = mother(Y, father(Z))

  5. mother(X, Y) = mother(Y, father(X))

  6. [X | Y] = [a, b, c]

  7. [X, Y | Z] = [a, b, c]

  8. add(add(1, 2), add(3, 4)) = add(X, add(Y, Z))

  9. add(X, add(Y, Z)) = add(add(X, Y), Z)

  10. p(X, Y, Z) = p(q(Y), r(Z), foo)

Solutions.

Here is a sorites (plural, soriteses) from Lewis Carroll:

  1. All my sons are slim.
  2. No child of mine is healthy who takes no exercise.
  3. All gluttons, who are children of mine, are fat.
  4. No daughter of mine takes any exercise.

This can be turned into a set of clauses in predicate calculus by

  1. using consistent terminology (fat = not slim, daughter = not son),
  2. changing each sentence into an implication, and
  3. changing implications into clauses by using the identity (A ⇒ B = ¬ A ∨ B).

(Note: ⇒ means implies, ¬means not, and ∨ means or.) So,

Statement

Implication

Clause

1. All my sons are slim.

son ⇒ slim

¬son ∨ slim

2. No child of mine is healthy who takes no exercise.

¬exercise ⇒ ¬healthy

exercise ∨ ¬healthy

3. All gluttons, who are children of mine, are fat.

glutton ⇒ ¬slim

¬glutton ∨ ¬slim

4. No daughter of mine takes any exercise.

¬son ⇒ ¬exercise

son ∨ ¬exercise

Resolve the following pairs of clauses:

Clauses to resolve

Resolution

1. ¬son ∨ slim
3. ¬glutton ∨ ¬slim

5.

1. ¬son ∨ slim
4. son ∨ ¬exercise

6.

2. exercise ∨ ¬healthy
4. son ∨ ¬exercise

7.

5.
7.

8.

Here, just for fun, is another sorites:

  1. Animals, that do not kick, are always unexcitable.
  2. Donkeys have no horns.
  3. A buffalo can always toss one over a gate.
  4. No animals that kick are easy to swallow.
  5. No hornless animal can toss one over a gate.
  6. All animals are excitable, except buffalo.

Solutions.

Resolve the following pairs of clauses:

Clauses to resolve

Resolution

1. ¬pass(X, history) ∨ ¬win(X, lottery) ∨ happy(X)
2. win(U, lottery) ∨ ¬lucky(U)

3.

3.
4. ¬happy(john)

5.

5.
6. lucky(john)

7.

7.
8. ¬lucky(V) ∨ pass(V, W)

9.

6. lucky(john)
9.

10.

Solutions.