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.

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.