Take-home Test, CS 156, due November 19, 2008

There are 100 points on the test

(10 points) Convert the predicate logic expression
```
(∀x) [ clear(x) ⊕ (∃y) on(y,x) ]
```
to clause form. Show your work. Hint: there are several ways to write the exclusive or operator in terms of and, or, and not.

(18 points) Find a resolution proof of the query (∃X) grandfather-of(X,X) from the knowledge base with the following clauses:

   1.  grandfather-of(X1,Y1) ∨ ¬father-of(X1,Z1) ∨ ¬parent-of(Z1,Y1)
   2.  grandfather-of(X2,Y2) ∨ ¬wife-of(W2,X2) ∨ ¬grandmother-of(W2,Y2)
   3.  grandmother-of(X3,Y3) ∨ ¬mother-of(X3,Z3) ∨ ¬parent-of(Z3,Y3)
   4.  grandmother-of(X4,Y4) ∨ ¬wife-of(X4,Z4) ∨ ¬grandfather-of(Z4,Y4)
   5.  parent-of(X5,Y5) ∨ ¬father-of(X5,Y5)
   6.  parent-of(X6,Y6) ∨ ¬wife-of(W6,X6) ∨ ¬mother-of(W6,Y6)
   7.  parent-of(X7,Y7) ∨ ¬mother-of(X7,Y7)
   8.  parent-of(X8,Y8) ∨ ¬wife-of(X8,Z8) ∨ ¬father-of(Z8,Y8)
   9.  wife-of(alice, bob)
  10.  wife-of(donna, calvin)
  11.  mother-of(alice, calvin)
  12.  mother-of(donna, bob)

Use a dummy answer predicate to find the final binding for X. Do not use Prolog notation for your clauses.

(10 points) For the knowledge base with clauses
```
  ¬gt(x,y) ∨ ¬gt(y,z) ∨ gt(x,z)
  ¬succ(a,b) ∨ gt(a,b)
  ¬gt(x,x)
```
why does the following attempt at a resolution proof of gt(5,2) run into problems? Here the predicate names gt and succ are abbreviations for is-greater-than and is-a-successor-of.
The negation of the query (omitting the quantifier ∀) is
0. ¬gt(5,2)
Assuming that the sentences of the knowledge base are numbered in order beginning with 1, then
Unifying 0 and 1 by the unifying substitution {5/x, 2/z}, we get
4. ¬gt(5,y) ∨ ¬gt(y,2)
Unifying 4 and 2 by the unifying substitution {y/a, 2/b}, we get
5. ¬gt(5,y) ∨ ¬succ(y,2)
Unifying 5 and 1 by the unifying substitution {5/x, y/z}, we get
6. ¬gt(5,y) ∨ ¬gt(y,y) ∨ ¬succ(y,2)
But now, since the middle disjunct is in the knowledge base, we cannot hope to derive a contradiction from this clause, regardless of whatever other clauses might be in the knowledge base.
(14 points) Assuming that p(d) = 0.0009, p(s1) = 0.1, p(s2) = 0.2, p(s1|d) = 0.9, p(s2|d) = 0.8, p(t) = 0.05, and p(t|s1) = 0.45, and that suitable independence assumptions hold, find the probability of the disease d given that
1. Both symptoms s1 and s2 are present.
2. Both symptoms s1 and s2 are absent.
(10 points) Using the assumptions of the previous problem, suppose that symptom s1 is not observable directly, but that test t is used as a test for it. What is the probability of the disease d given a negative result for test t? Note that you may ignore symptom s2 in your computation.

(10 points) For each of the two previous problems, what independence assumption(s) did you make?

In Problems 7 and 8, assume that the following three actions are available. Each action is given with its precondition (prerequisite) list, addlist, and deletelist, in that order.

moveToTable(?x): 
  [on(?x, ?y), clear(?x)],
  [ontable(?x), clear(?y)],
  [on(?x, ?y)]
moveFromTable(?x,?y):
  [ontable(?x), clear(?x), clear(?y)]
  [on(?x, ?y)]
  [ontable(?x), clear(?y)]
move(?x, ?z):
  [on(?x, ?y), clear(?x), clear(?z)]
  [on(?x, ?z), clear(?y)]
  [on(?x, ?y), clear(?z)]

(18 points)
1. (6 points) Using the actions given above, find a plan to achieve the goal on(c,a) ^ on(a,b) from the state whose complete description is [clear(a), ontable(a), clear(b), on(b,c), ontable(c)] Express your plan as a list of instantiated actions. You needn't use any particular algorithm to find the plan.
2. (12 points) For each action in your plan, verify that the prerequisites of the action are met when it is applied, and give a complete state description on the resulting state. Verify that the goal is met by the final state.
(10 points) Show that the predicate given below is an invariant of the blocks world with the 3 actions given above. That is, show that whenever the invariant is true in state S, A is a sequence of actions, and each action in A is an instantiated version of one of the three actions given above then the invariant is true in the state that results from applying the actions of A, in order, to state S. For full credit, your proof should be by induction. The proposed invariant is (∀?x) [(clear(?x) ⊕ (∃?y) on(?y, ?x)) ^ (ontable(?x) ⊕ (∃?z) on(?x, ?z))] You may assume that no action attempts to place a block on top of itself.