Resolution practice--problems

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

foo(X, Y) = foo(a, a) foo(X, Y) = foo(a, X) foo(X, Y) = foo(Y, X) mother(mary, X) = mother(Y, father(Z)) mother(X, Y) = mother(Y, father(X)) [X | Y] = [a, b, c] [X, Y | Z] = [a, b, c] add(add(1, 2), add(3, 4)) = add(X, add(Y, Z)) add(X, add(Y, Z)) = add(add(X, Y), Z) 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 v B).

(Note: I'm using => for implies, - for not, and v for or.) So,

Statement	Implication	Clause
1. All my sons are slim.	son => slim	-son v slim
2. No child of mine is healthy who takes no exercise.	-exercise => -healthy	exercise v -healthy
3. All gluttons, who are children of mine, are fat.	glutton => -slim	-glutton v -slim
4. No daughter of mine takes any exercise.	-son => -exercise	son v -exercise

Resolve the following pairs of clauses:

Clauses to resolve	Resolution
1. -son v slim 3. -glutton v -slim	5.
1. -son v slim 4. son v -exercise	6.
2. exercise v -healthy 4. son v -exercise	7.
5. 7.	8.

Here, just for fun, is another sorites:

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

Solutions.

Resolve the following pairs of clauses:

Clauses to resolve	Resolution
1. -pass(X, history) v -win(X, lottery) v happy(X) 2. win(U, lottery) v -lucky(U)	3.
3. 4. -happy(john)	5.
5. 6. lucky(john)	7.
7. 8. -lucky(V) v pass(V, W)	9.
6. lucky(john) 9.	10.

Solutions.