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.