Blocks world axioms: Style 2
Sorts
The sort of a variable is indicated by its first letter:
Objects (blocks and table) (O,X,Y,Z) ; situations (S); fluents (F);
actions (A).
Nonlogical primitives
Atemporal:
 block(X). Predicate: X is a block.
 table. Constant: The table.
Fluents
 on(X,Y). Function. The fluent of object X being on object Y.
 clear(X). Function. The fluent of object X being clear.
Actions
 puton(X,Y). Function. The action of putting X onto Y.
Situation calculus
 holds(S,F). Predicate: Fluent F holds in situation S.
 result(S,A). Function: The situation that results if action A is performed
in situation S.
 poss(S,A). Predicate: Action A is possible in situation S.
Axioms
Atemporal axiom
 1. forall_{O} block(O) xor O=table.
State coherence axioms (Domain constraints)
Note: The axioms below are not complete; indeed there does not exist
a complete firstorder axiomatization using the above primitives.
However, these axioms are sufficient to do prediction.
 2. forall_{S,X} block(X) =>
exists^{1}_{Y} holds(S,on(X,Y)).
(A block is always on a unique other object.)
 3. forall_{S,X,Y,Z} block(X) ^ holds(S,on(Y,X)) ^
holds(S,on(Z,X)) => Z=Y
(At most one object can be on block X in situation S.)
 4. forall_{S,X,Y} holds(S,on(X,Y)) => block(X) ^ X != Y.
(Only a block can be on another object. A block cannot be on itself.)
 5. forall_{S,X} holds(S,clear(X)) < = >
block(X) ^ ~exists_{Y} holds(S,on(Y,Z)).
(Definition of clear: A block is clear if there's nothing on it.)
Causal axiom
 6. forall_{S,X,Y}
poss(S,puton(X,Y)) => holds(result(S,puton(X,Y)),on(X,Y))
Frame axiom
 7. forall_{S,X,Y,W,Z}
[ (W=X ^ Z=Y) V
(W=X ^ holds(S,on(W,Z)) V
holds(result(S,puton(X,Y)),on(W,Z)) < = > holds(S,on(W,Z))
The fluent "on(W,Z)" does not change as a result of the action
"puton(X,Y) unless either W=X and Z=Y or W=X and Z is the object
that X was on initially.
Feasibility axiom

8. poss(S,puton(X,Y)) < = > X !=Y ^
holds(S,clear(X)) ^ [holds(S,clear(Y)) V
Y=table].
It is possible to put X onto Y iff X is clear and either Y is clear or
Y is the table.
Unique names
Sample inference
Scenario: a,b,c are blocks. In the initial situation s0, a is on c;
b and c are on the table. You then move a to b.
 P1: holds(s0,on(a,c)).
 P2: holds(s0,on(b,table)).
 P3: holds(s0,on(c,table)).
 P4: holds(s0,clear(a)).
 P5: holds(s0,clear(b)).
 P6: holds(s0,block(a)).
 P7: holds(s0,block(b)).
 P8: holds(s0,block(c)).
 P9: s1 = result(s0,puton(a,b)).
 P10: a != b !=c !=a.
(Note that nothing in these rules out the possibility of other blocks
being elsewhere on the table.)
We wish to derive a complete characterization of the state of the world
after putting a onto b. Specifically, we need to prove.
holds(s1,on(a,b)).
holds(s1,clear(a)).
holds(s1,clear(c)).
holds(s1,on(b,table))
holds(s1,on(c,table))
Proof:
(Asterisk indicate parts of the result to be proven.)
S1: poss(s0,puton(a,b)). (From 8, P4, P4, P10).
S2*: holds(s1,on(a,b)). (From 6, S1).
S3: forall_{X} ~holds(s0,on(X,a)). (From P4, 5).
S4: forall_{X} ~holds(s1,on(X,a)). (From S3, P10, 7)
S5*: holds(s1,clear(a)). (From S4, 5).
S6: ~holds(s1,on(a,c)). (From S2, P10, 2).
S7: forall_{X} X !=a => ~holds(s0,on(X,c)). (From P1,2).
S8: forall_{X} X !=a => ~holds(s1,on(X,c)). (From S7,7).
S9: forall_{X} ~holds(s1,on(X,c)). (From S6, S8)
S10*: holds(s1,clear(c)). (From S4, 5).
S11: table !=b. (From P7, 1)
S12*: holds(s1,on(b,table)). (From P2,S11,7)
S13*: holds(s1,on(c,table)). (From P2,S11,7)