Artificial Intelligence: Problem Set 3

Assigned: Feb. 22
Due: Mar. 7

Consider a domain whose entities are people. Let L be the first-order language containing the following predicates:

e(X) --- X is male.
f(X) --- X is female.
p(X,Y) -- X is a parent of Y
m(X,Y) -- X is a mother of Y
f(X,Y) -- X is a father of Y
g(X,Y) -- X is a grandparent of Y
t(X) --- X is tall.

Problem 1

Express the following sentences in L.

Problem 2

Convert sentences 1-6 above to clausal form. You need not show the intermediate steps of Skolemization.

Problem 3

Using resolution, prove 7 and 8 from axioms 1-6. You must show the Skolemized form of the negated goals and each step of the resolution proof. You need not show the intermediate steps of Skolemization.

Problem 4

Statement 9 above can be proven from the Horn clauses that appear in the Skolemization of sentences 1-6. Give a backwards chaining proof of 9 and a forward chaining proof of 9.

Back to course home page