Assigned: Feb. 27 Due: Mar. 20

Consider a domain whose entities are people, books, and volumes.
(A "volume" is a particular physical object, which is a copy of an
abstract "book", like *Moby Dick*).

Let L be the first-order language containing the following predicates:

o(P,V) --- Predicate. Person P owns volume V

c(V,B) --- Predicate. Volume V is a copy of book B.

a(P,B) --- Predicate. Person P is the author of book B.

i(P,B) --- Predicate. Person P is the illustrator of book B.

h --- Constant. Howard Pyle.

s --- Constant. Sam.

j --- Constant. Joe.

- a. Sam owns a copy of every book that Howard Pyle illustrated.

**Answer:**forall(B) i(h,B) => exists(V) o(s,V) ^ c(V,B). - b. Joe owns a copy of a book that Howard Pyle wrote.

**Answer:**exists(V,B) o(j,V) ^ c(V,B) ^ a(h,B). - c. Howard Pyle illustrated every book that he wrote.

**Answer:**forall(B) a(h,B) => i(h,B). - d. Sam owns only illustrated books. Interpret this in the form
"If Sam owns volume V and V is a copy of book B, then B has been
illustrated by someone."

**Answer:**forall(V,B) o(s,V) ^ c(V,B) => exists(P) i(P,B) - e. None of the books that Joe has written have been illustrated by anyone.

**Answer:**not exists(B,P) a(j,B) ^ i(P,B). - f. Sam does not own a copy of any book that Joe has written.

**Answer:**forall(B) a(j,B) => not exists(V) c(V,B) ^ o(s,B). - g. There is a book
*B*such that both Sam and Joe own a copy of*B*.

**Answer:**exists(B,V1,V2) c(V1,B) ^ o(s,V1) ^ c(V2,B) ^ o(j,V2).

Answer: Skolemizing (a-c) gives the following clauses.

a1: -i(h,B) V o(s,sk1(B)). a2: -i(h,B) V c(sk1(B),B) b1: o(j,sk2). b2: c(sk2,sk3) b3: a(h,sk3) c1: -a(h,B) V i(h,B).

The Skolemized form of the negation of (g) is

g1: -c(V1,B) V -o(s,V1) V - c(V2,B) V -o(j,V2).

One resolution proof proceeds as follows:

h: -c(V1,B) V -o(s,V1) V -c(sk2,B). (From g1 and b1, V2 -> sk2) i: -c(V1,sk3) V -o(s,V1). (From h and b2, B -> sk3) j: i(h,sk3) (From b3 and c1, B -> sk3) k: o(s,sk1(sk3)). (From j and a1, B -> sk3) l: c(sk1(sk3),sk3). (From j and a2, B-> sk3). m: -o(s,sk1(sk3)). (From l and c, V1 -> sk1(sk3)) n: empty (From m and k)

The Skolemized forms of (d,e) are

d1: -o(S,V) V -c(V,B) V i(sk4(V,B),B) e1: -a(j,B) V -i(P,B)

(Alternative answer for d1: d can be rewritten in the logically
equivalent form

forall(B) [exists(V) o(s,V) ^ c(V,B)] => exists(P) i(P,B).

This form reveals that P does not actually depend on V. Applying the
Skolemization procedure to this form gives

d1': -o(S,V) V c(V,B) V i(sk4(B),B)In terms of finding resolution proofs, it makes no difference which of these is used.)

The Skolemized form of the negation of f is

f1: a(j,sk5) f2: c(sk6,sk5) f3: o(s,sk6)

One resolution proof proceeds as follows:

p: -c(sk6,B) V i(sk4(sk6,B),B) (From f3 and d1, V -> sk6) q: i(sk4(sk6,sk5),sk5) (From f2 and p, B -> sk5). r: -a(j,sk5). (From q and e1, B -> sk5, P -> sk4(sk6,sk5)) s: empty (From r and f1).