Answer to Shakey's problem using the successor state formulation

General comments:  
* every variable has to be quantified, either universally over the entire
  expression or existentially.
* you need at least one axiom per predicate, to describe the conditions
  that make the predicate true in the result of doing an action
* you need to ensure that each of the action is covered in one or more 
  axioms, otherwise when the action is done we will not know what is true 
  in the resulting situation
* you have to be consistent with the names of predicates and actions.  In
  the formulation given when Shakey is On a box, Shakey is no longer At
  a location, but the box is still At the location.  When Shakey is At a
  location, it is On the floor, so we should add On(Shakey,Floor, S0) to 
  the description of the initial situation S0. 


1. Shakey goes from x to y
   forall x,y,z,a,s ->
     At(Shakey,y,Result(a,s)) <=> [At(Shakey,x,s) ^ a=Go(x,y)]
				  V
			          [At(Shakey,y,s) ^ a!=Go(y,z)]

2. Shakey pushes a box from x to y
This next axiom is more complex than the others, since when a box is 
pushed both the box and Shakey end up in position z.  We can write it
as as single axiom or as two separate axioms

   forall b,x,y,z,a,s ->
   At(b,y,Result(a,s)) ^ At(Shakey,y,Result(a,s))
			      <=> [Box(b) ^ At(b,x,s)) ^ At(Shakey,x,s) 
			           ^ a=Push(b,x,y)]
                                  V
                                  [At(b,y,s) ^ At(Shakey,y,s) ^ a!=Push(b,y,z)
				   ^ a!=Go(y,z)]
or, as two axioms

forall b,x,y,z,a,s ->
   At(b,y,z,Result(a,s))      <=> [Box(b) ^ At(b,x,s)) ^ At(Shakey,x,s) 
			           ^ a=Push(b,x,y)]
                                  V
                                  [At(b,y,s) ^ a!=Push(b,y,z)]

forall b,x,y,z,a,s ->
   At(Shakey,y,z,Result(a,s))  <=> [Box(b) ^ At(b,x,s)) ^ At(Shakey,x,s) 
			           ^ a=Push(b,x,y)]
                                  V
                                  [At(Shakey,y,s) ^ a!=Push(b,y,z) ^
				  a!=Go(y,z)]
3. Shakey climbs a box
   forall x,b,a,s ->
     On(Shakey,b,Result(a,s)) <=> [(At(Shakey,x,s) ^ On(Shakey,Floor,s) 
				   ^ Box(b) ^ At(b,x,s) ^ a=Climbup(b)]
                                  V
                                  [On(Shakey,b,s) ^ a!=ClimbDown(b)]

4. Shakey climbs down a box
   forall a,s ->
  On(Shakey,Floor,Result(a,s)) <=> [exists b Box(b) ^ On(Shakey,b,s) 
				    ^ a=ClimbDown(b)]
				   V
                                   [On(Shakey,Floor,s) ^ a!=Climbup]

5. Shakey turns on the light
   forall l,a,s ->
     LightOn(l,Result(a,s))    <=> [exists b,x Box(b) ^ On(Shakey,b,s) 
				    ^ At(l,x,s) ^ At(b,x,s) ^ a=TurnOn(l)]
				   V
                                   [LightOn(l,s) ^ a!=TurnOff(l)]

6. Shakey turns off the light
   forall l,a,s ->
   LightOff(l,Result(a,s))      <=> [exists b,x Box(b) ^ On(Shakey,b,s)
				     ^ At(l,x,s) ^ At(b,x,s) ^ a=TurnOff(l)]
				    V 
				    [LightOff(l,s) ^ a!=TurnOn(l)]