CMSC 471

Artificial Intelligence -- Fall 2004

HOMEWORK FOUR
out 10/14/04; due 10/28/04

 

I. Knowledge-Based Agents (15 points)

Russell & Norvig Exercise 7.1.  Note: Use the description of the Wumpus world from the book (not the online variations that we saw in class).

II. Logic (55 points)

(a) Russell & Norvig Exercise 7.5.  (15 pts)

(b) Russell & Norvig Exercise 7.6 (b,c).  (15 pts)

(c) Russell & Norvig Exercise 7.11 (a).  (10 pts)

(d) Russell & Norvig Exercise 8.6 (a,b,c,i,j). (15 pts)

III. Resolution Theorem Proving (30 points)


(a) (8 points) Represent the following knowledge base in first-order logic.  Use the predicates

where arguments x have the domain of all people, and arguments t have the domain of all tests.
  1. Everyone who is smart, studies, and attends class will be prepared.
  2. Everyone who is prepared will pass a test if it is fair.
  3.  A student passes a test if and only if they don't fail it.
  4.  Every UMBC student is smart.
  5.  If a test isn't fair, everyone will fail the test.
  6.  Aidan is a UMBC student.
  7.  Sandy passed the 471 exam.
  8.  Aidan attends class.

(b) (8 points) Convert the KB to conjunctive normal form.

(c) (2 points) We wish to prove that

study(Aidan) -> pass(Aidan, 471-exam)

Express the negation of this goal in conjunctive normal form.

(c) (12 points) Add the negated goal to the KB, and use resolution refutation to prove that it is true. You may show your proof as a series of sentences to be added to the KB or as a proof tree.  In either case, you must clearly show which sentences are resolved to produce each new sentence, and what the unifier is for each resolution step.