| The following is an example of an axiom we would like | to encode: | | Forall x. Forall s. | holding( x,do( a,s ) ) iff | [( a=pickup( x) ) V ( holding( x,s ) & ( a neq putdown( x) )] | Legend: | - do is a function that maps actions ( a) and situations ( s) into | new situations ( s) . | - V is ''or'' | - neq is ''not equal'' | - iff is ''if and only if'' | | This axiom says | holding x in the situation resulting from | performing action a in situation s ( i.e., ''do( a,s ) '' ) if and only if | - the action was ''pickup( x) '' | OR | - holidng x is situation s, and the action was | not ''putdown( x) '' some-number is a situation id some-actor is a robot some-item is a block pickup could be applied to a block not : in the situation that-number that-actor is holding that-item that-number + 1 = some-number1 --------------------------------------------------------------------------------------------------------- starting from sit that-number and doing pickup results in sit that-number1 with the robot holding that-item in the situation some-number some-robot is holding some-item some-verb is an action not : that-verb is equal putdown not : that-verb is equal pickup that-number + 1 = some-number1 -------------------------------------------------------------------------------------------------------------- starting from sit that-number and doing that-verb results in sit that-number1 with the robot holding that-item this-action could be applied to a block ======================================== pickup putdown this-number is a situation id ============================= 9 this-verb is an action ====================== pickup putdown Go to home position some-item is a block ==================== A B this-actor is a robot ===================== R1 in the situation this-situation this-robot is holding this-item ================================================================ 1 R1 A