CIS 554 Solutions to Resolution Practice Problems
Fall 2012, 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.