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.

Answer:

Converting (1-4) and the negation of (5) to CNF gives: 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:

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.