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.
Answer:
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.
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.