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).

Non-logical primitives

Atemporal:

Fluents

Actions

Situation calculus

Axioms

Atemporal axiom

State coherence axioms (Domain constraints)

Note: The axioms below are not complete; indeed there does not exist a complete first-order axiomatization using the above primitives. However, these axioms are sufficient to do prediction.

Causal axiom

Frame axiom

Feasibility axiom

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. (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: forallX ~holds(s0,on(X,a)). (From P4, 5).
S4: forallX ~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: forallX X !=a => ~holds(s0,on(X,c)). (From P1,2).
S8: forallX X !=a => ~holds(s1,on(X,c)). (From S7,7).
S9: forallX ~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)