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

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