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) {x/A, y/B, z/B}
   2. Q(y,G(A,B)), Q(G(x,x),y) The text says that 'No unifier (x cannot bind to both A and B)’:
          Q(G(x,x),G(A,B)), Q(G(x,x),G(x,x))  {y/G(x,x)}
          Q(G(x,x),G(A,B)), Q(G(x,x),G(A,B))  {x/A, x/B}
      However, can unify if standardize apart the two y variables before unification:
          Q(z,G(A,B)) and Q(G(x,x),y)
          Q(G(x,x),G(A,B)), Q(G(x,x),G(A,B)) {z/G(x,x), y/G(A,B)}
   3. Older(Father(y),y),Older(Father(x),John) {y/John, x/John}
   4. Knows(Father(y),y)), Knows(x,x) No unifier (because occurs-check prevents unification of y with Father(y); y occurs in term Father(y))
       
2. (3) Convert to CNF:   
   
   "x{ØP(x) Ú {"y[P(y) Þ P(f(x,y))] Ù $w[Q(x,w) Ù ØP(w)]}}
   
   "x{ØP(x) Ú {"y[ØP(y) Ú P(f(x,y))] Ù $w[Q(x,w) Ù ØP(w)]}}   Implication elimination
   
   "x{ØP(x) Ú {"y[ØP(y) Ú P(f(x,y))] Ù [Q(x, h(x)) Ù ØP(h(x))]}}  Eliminate $w Skolemize
   
   "x"y{[ØP(x) Ú ØP(y) Ú P(f(x,y))] Ù [ØP(x) Ú Q(x, h(x))] Ù [ØP(x) Ú ØP(h(x))]}  distribute ØP(x)
   
   [ØP(x) Ú ØP(y) Ú P(f(x,y))] Ù [ØP(x) Ú Q(x, h(x))] Ù [ØP(x) Ú ØP(h(x))]   Eliminate "
   
   
    
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)
   • • ØAbove(B, y) Ú ØAbove(y, Table) Ú Above(B,Table)   {x/B, z/Table}
     •                                                  ØAbove(B, Table)
     • ØAbove(B, y) Ú ØAbove(y, Table)
        
     • ØOn(u, Table) Ú Above(u, Table)                              {u/B, v/A}
     • ØAbove(B, y) Ú ØAbove(y, Table)
     • ØOn(y, Table) Ú ØAbove(B, y)
        
     • ØOn(B, y) Ú Above(B, y)                                         {u/B}
     • ØOn(y, Table) Ú ØAbove(B, y)
     • ØOn(B, y) Ú ØOn(y, Table)
        
     • On(B, A)
     • ØOn(B, y) Ú ØOn(y, Table)                                       {y/A}
     • ØOn(A, Table)
        
     • ØOn(A, Table)
     • 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)
      

   Facts	Goals	Rule	Substitution
   On(B,A), On(A,Table)	Above(B, Table)	Above(B, y) Ù Above(y, Table)                 Þ Above(B,Table)	{x/B, z/Table}
   On(B,A), On(A,Table)	Above(B, y), Above(y, Table), Above(B,Table)	On(B,v) Þ Above(B,v)	{u/B, v/y}
   On(B,A), On(A,Table)	On(B,y), Above(B,y), Above(y,Table),Above(B,Table)	On(B,A)	{y/A}
   On(B,A), On(A,Table)	Above(B,y), Above(y,Table), Above(B,Table)	On(B,A) Þ Above(B,A)	{y/A}
   On(B,A), On(A,Table), Above(B,A)	Above(y,Table), Above(B,Table)	On(y,Table) Þ Above(y, Table)	{u/y, v/Table}
   On(B,A), On(A,Table), Above(B,A)	Above(B,Table)	On(A,Table) Þ Above(A, Table)	{y/A}
   On(B,A), On(A,Table), Above(B,A),Above(A,Table)	Above(B,Table)	Above(B, A) Ù Above(A, Table)                  Þ Above(B, Table)

    

5. (3) Give the STRIPS operations to move blocks from the Initial to Goal state.

 

Final plan is: b = Move(C, A, Table), c = Move(B, Table, C), a = Move(A, Table, B).

b c a

By regression:

Initial state:

On(A, Table) Ù On(B, Table) Ù On(C, A) Ù Block(A) Ù Block(B) Ù Block(C)
Ù Clear(B) Ù Clear(C)

Goal state:

On(C, Table) Ù On(B, C) Ù On(A,B)
Ù Block(A) Ù Block(B) Ù Block(C) Ù Clear(A)

Action( Move(b, x, y),    Move block b from x to y
    Precond: On(b, x) Ù Clear(b) Ù Clear(y) Ù Block(b)
    Effect:    On(b, y) Ù Clear(x)
 

---

Action( Move(A,Table,B),
    Precond: On(A,Table) Ù Clear(A) Ù Clear(B) Ù Block(A)
    Effect:    On(A, B) Ù Clear(Table) )

State:
    On(C, Table) Ù On(B, C) Ù On(A,Table) Ù Clear(B)
    Ù Block(A) Ù Block(B) Ù Block(C) Ù Clear(A)

---

Action( Move(B,Table,C),
    Precond: On(B, Table) Ù Clear(B) Ù Clear(C) Ù Block(B)
    Effect:    On(B,C) Ù Clear(Table)

State:
    On(C, Table) Ù On(B, Table) Ù On(A,Table) Ù Clear(B)
    Ù Block(A) Ù Block(B) Ù Block(C) Ù Clear(A) Ù Clear(C)

---

Action( Move(C,A,Table),
    Precond: On(C, A) Ù Clear(C) Ù Clear(Table) Ù Block(C)
    Effect:    On(C, Table) Ù Clear(A)

State:
    On(A,Table) Ù On(B, Table) Ù On(C,A) Ù Block(A) Ù Block(B) Ù Block(C)
    Ù Clear(B) Ù Clear(C)

---

Initial state:

On(A, Table) Ù On(B, Table) Ù On(C, A) Ù Block(A) Ù Block(B) Ù Block(C)
Ù Clear(B) Ù Clear(C)