Resolution Practice--Solutions to problems
Fall 2011, David Matuszek

Problems.

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

    X = Y = a


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

    X = Y = a


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

    X = Y


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

    Y = mary, X = father(Z)


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

    X = Y = father(X), or more accurately,
    X = Y = father(father(father(father(...))))
    (This is a recursive data structure that is legal but not recommended.)


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

    X = a, Y = [b, c]


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

    X = a, Y = b, Z = [c]


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

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


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

    X = add(X, Y), Z = add(Y, Z), that is,
    X = add(add(add(..., Y), Y), Y), Z = add(Y, add(Y, add(Y, ...)))


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

    X = q(r(foo)), Y = r(foo), Z = foo

Clauses to resolve

Resolution

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

5. ¬son ∨ ¬glutton

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

6. slim ∨ ¬exercise

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

7. son ∨ ¬healthy

5. ¬son ∨ ¬glutton
7. son ∨ ¬healthy

8. ¬glutton ∨ ¬healthy
"Those of my children, who are gluttons, are not healthy."

Donkeys are not easy to swallow.

Clauses to resolve

Resolution

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

3. ¬pass(U, history) ∨ happy(U) ∨ ¬lucky(U)
or equivalently:
¬pass(X, history) ∨ happy(X) ∨ ¬lucky(X)

3. ¬pass(U, history) ∨ happy(U) ∨ ¬lucky(U)
4. ¬happy(john)

5. ¬pass(john, history) ∨  ¬lucky(john)

5. ¬pass(john, history) ∨ ¬lucky(john)
6. lucky(john)

7. ¬pass(john, history) 

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

9. -lucky(john)

6. lucky(john)
9. -lucky(john)

10. The result is NIL, the empty clause. This indicates that the clauses that were resolved to get to this point are inconsistent.