## 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.

The statement of the above assertions, as given in solution set 3 was:
• 1. forall(X,Y) mo(X,Y) <=> fe(X) ^ p(X,Y).
• 2. forall(X,Y) fa(X,Y) <=> ~fe(X) ^ p(X,Y).
• 3. forall(X) o(X) <=> ~(exists (Y) p(Y,X) ^ a(Y)).
• 4. ~o(s).
• 5. (exists(X) a(X) ^ fa(X,s)) V (exists(X) a(X) ^ mo(X,s)).
• 6. forall(X) exists(Y,Z) fa(Y,X) ^ mo(Z,X).
Converting (1-4) and the negation of (5) to CNF gives:
• 1.A. ~mo(X,Y) V fe(X).
• 1.B. ~mo(X,Y) V p(X,Y).
• 1.C. ~fe(X) V ~p(X,Y) V mo(X,Y).
• 2.A. ~fa(X,Y) V ~fe(X).
• 2.B. ~fa(X,Y) V p(X,Y).
• 2.C. fe(X) V ~p(X,Y) V fa(X,Y).
• 3.A. ~o(X) V ~p(Y,X) V ~a(Y).
• 3.B. o(X) V p(sk(X),X).
• 3.C. o(X) V a(sk(X)).
• 4. ~o(s).
• 5. (exists(X) a(X) ^ fa(X,s)) V (exists(X) a(X) ^ mo(X,s)).
• 5.A. ~a(X) V ~fa(X,s).
• 5.B. ~a(X) V ~mo(X,s).
One resolution proof proceeds as follows
Resolving 4 with 3.B gives      D. p(sk(s),s).
Resolving 4 with 3.C gives      E. a(sk(s)).
Resolving D with 1.C gives      F. ~fe(sk(s)) V mo(sk(s),s).
Resolving D with 2.C gives      G. fe(sk(s)) V fa(sk(s),s).
Resolving F and G gives         H. mo(sk(s),s) V fa(sk(s),s).
Resolving H with 5.A gives      I. ~a(sk(s)) V mo(sk(s)).
Resolving I with 5.b gives      J. ~a(sk(s)) V ~a(sk(s))
Factoring J gives               K. ~a(sk(s)).
Resolving K with E gives the null clause.

### Problem 2

Give a resolution proof of (4) from 1,2,3,5.

Answer: Converting (1-3,5) and the negation of (4) to CNF gives:

• 1.A. ~mo(X,Y) V fe(X).
• 1.B. ~mo(X,Y) V p(X,Y).
• 1.C. ~fe(X) V ~p(X,Y) V mo(X,Y).
• 2.A. ~fa(X,Y) V ~fe(X).
• 2.B. ~fa(X,Y) V p(X,Y).
• 2.C. fe(X) V ~p(X,Y) V fa(X,Y).
• 3.A. ~o(X) V ~p(Y,X) V ~a(Y).
• 3.B. o(X) V p(sk(X),X).
• 3.C. o(X) V a(sk(X)).
• 4. o(s).
• 5.A. a(sk1) V a(sk2).
• 5.B. a(sk1) V mo(sk2,s).
• 5.C. fa(sk1,s) V a(sk2).
• 5.D. fa(sk1,s) V mo(sk2,s).
Resolving 4 with 3.A gives          E. ~p(Y,s) V ~a(Y).
Resolving E with 1.B gives          F. ~mo(Y,s) V ~a(Y).
Resolving E with 2.B gives          G. ~fa(Y,s) V ~a(Y).
Resolving F with 5.B gives          H. a(sk1) V ~a(sk2).
Resolving H with 5.A gives          I. a(sk1) V a(sk1)
Factoring I gives                   J. a(sk1)
Resolving J with G gives            K. ~fa(sk1,s).
Resolving K with 5.D gives          L. mo(sk2,s).
Resolving L with F gives            M. ~a(sk2).
Resolving K with 5.C gives          N. a(sk2).
Resolving M and N gives the null clause.