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

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

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.