## Problem Set 4

Assigned: Mar. 1.

Due: Mar. 22.
In problem set 3, problem 2, you were asked the following:

Consider a first-order language L over a universe of people with the
following primitives:
p(X,Y) --- Predicate. X is a parent of Y.

fa(X,Y) --- Predicate. X is a father of Y.

mo(X,Y) --- Predicate. X is a mother of Y.

fe(X) --- Predicate. X is female

a(X) --- Predicate. X is alive.

o(X) --- Predicate. X is an orphan.

s,a,b --- Constant. Sarah, Andy, Bob.

Express the following statements in L.

- 1. A mother is a female parent.
- 2. A father is a parent who is not female.
- 3. An orphan is someone with no living parents.
- 4. Sarah is not an orphan.
- 5. Sarah either has a living father or a living mother.
- 6. Everyone has a father and a mother.

### Problem 1

Give a resolution proof of (5) from (1-4). Note: You need not show the
intermediate stages of the conversion to CNF. You must show every
resolution in the proof. The proof must be a resolution proof.
### Problem 2

Give a resolution proof of (4) from 1,2,3,5.
NOTE: The solution to problem set 3 will be posted on or about March 8.
If you are not confident of your own solution to problem 2, you might
want to hold off until then, so that you can be sure of starting from
the correct statement of the axioms.

###
Problem 3

Trace the action of the Davis-Putnam algorithm on the following clauses
1. ~P V Q.

2. ~P V R.

3. P V ~Q V R.

4. ~R V S.

5. R V ~S.

6. ~P V ~S.

7. ~P V ~Q V S.