Resolution practice--solutions

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 v slim
3. -glutton v -slim

5. -son v -glutton

1. -son v slim
4. son v -exercise

6. slim v -exercise

2. exercise v -healthy
4. son v -exercise

7. son v -healthy

5. -son v -glutton
7. son v -healthy

8. -glutton v -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) v -win(X, lottery) v happy(X)
2. win(U, lottery) v -lucky(U)

3. -pass(U, history) v happy(U) v -lucky(U)
or equivalently
-pass(X, history) v happy(X) v -lucky(X)

3. -pass(U, history) v happy(U) v -lucky(U)
4. -happy(john)

5. -pass(john, history) v  -lucky(john)

5. -pass(john, history) v -lucky(john)
6. lucky(john)

7. -pass(john, history) 

7. -pass(john, history))
8. -lucky(V) 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.