## Artificial Intelligence: Problem Set 3

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.

### Problem 1

Express the following statements in L: (Note correction to sentence d.)
• 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.
• 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).

### Problem 2

Using resolution, show that (g) can be proven from (a-c) and that (f) can be proven from (d,e). You must show the Skolemized form of each of the axioms and of the negated goals. You need not show the intermediate steps of Skolemization.

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).
```