## 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:

• 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. forallO block(O) xor O=table.

#### 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.
• 2. forallS,X block(X) => exists1Y holds(S,on(X,Y)).
(A block is always on a unique other object.)
• 3. forallS,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. forallS,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. forallS,X holds(S,clear(X)) < = > block(X) ^ ~existsY holds(S,on(Y,Z)).
(Definition of clear: A block is clear if there's nothing on it.)

#### Causal axiom

• 6. forallS,X,Y poss(S,puton(X,Y)) => holds(result(S,puton(X,Y)),on(X,Y))

#### Frame axiom

• 7. forallS,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.

### 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: 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)