Exercise 8        Name __________________        Score __/17

1. (4) Some of the following may not unify, state why not or give the MGU of:
   1. P(A,B,B), P(x,y,z)
   2. Q(y,G(A,B)), Q(G(x,x),y)
   3. Older(Father(y),y),Older(Father(x),John)
   4. Knows(Father(y),y)), Knows(x,x)

    

2. (3) Convert to CNF:    "x{P(x) Þ {"y[ØP(y) Ú P(f(x,y))] Ù $w[Q(x,w) Ù ØP(w)]}}
   
    
3. (4) Prove using resolution: Above(B, Table)
   • ØOn(u, v) Ú Above(u, v)
   • ØAbove(x, y) Ú ØAbove(y, z) Ú Above(x, z)
   • On(B, A)
   • On(A, Table)
     
      
4. (3) Prove using backward chaining: Above(B, Table)
   • ØOn(u, v) Ú Above(u, v)
   • ØAbove(x, y) Ú ØAbove(y, z) Ú Above(x, z)
   • On(B, A)
   • On(A, Table)
      
5. (3) Give the STRIPS operations to move blocks from the Initial to Goal state.

Initial                                                                             Goal