# Simple axiomatization of the blocks world

```% ----- initial situation s0 ------
%
%  blocks on table layed out thus:
%
%           c
%   a   b   d
%  ------------------------------
%
% in "holds(X,Y)"  X says something X about the blocks world
% and Y describes the state we have arrived to via robot actions from the original state
%
% s0 is our name for the initial state.
%
% "clear(X)" means that someting can be put on X
% "holds(empty,Y)" means that the robot hand is empty in state Y.
% ---------------------------------------------------------------

holds(on(a,table),s0).

holds(on(b,table),s0).

holds(on(c,d),s0).

holds(on(d,table),s0).

holds(clear(a),s0).

holds(clear(b),s0).

holds(clear(c),s0).

holds(empty,s0).

holds(clear(table),State).

% ---- difference of objects -----
%
% By default we do not know that "a" and "b" denote different blocks.
% Could well be that they are two labels of the same block.
%
% Instead of "differ(X,Y)" we could axiomatize that they are not equal, using
% "X != Y" but equality allows to derive a lot of additional stuff, bogging down
% proof search. Here we use a simpler axiomatizon of being different.
%
% Difference of "a" and "b" etc is used both in the robot arm axioms
% and the frame axioms in the following
%
% ---------------------------------

differ(X,Y)
| -differ(Y,X).

differ(a,b).

differ(a,c).

differ(a,d).

differ(a,table).

differ(b,c).

differ(b,d).

differ(b,table).

differ(c,d).

differ(c,table).

differ(d,table).

% ------- logic additionally encoded in terms -----
% we are not using a special "and" function, but if we wanted to,
% this would be one way to say it:
%
%holds(and(X,Y),State)
%    | -holds(X,State)
%    | -holds(Y,State).
% -----------------------------------------------

% ----- pickup rules  ------
%
% These say what conditions must hold for the robot hand to pick
% up something and what happens to the state when the action
% is done.
%
% ---------------------------

holds(holding(X),do(pickup(X),State))
| -holds(empty,State)
| -holds(clear(X),State)
| -differ(X,table).

holds(clear(Y),do(pickup(X),State))
| -holds(on(X,Y),State)
| -holds(clear(X),State)
| -holds(empty,State).

% -----------------------
% frame axioms for pickup
%
% Saying that if something is picked up, most of the things which did
% hold in the previous state will still hold in the new state
%
% Notice the use of "differ".
% -----------------------

holds(on(X,Y),do(pickup(Z),State))
| -holds(on(X,Y),State)
| -differ(X,Z).

holds(clear(X),do(pickup(Z),State))
| -holds(clear(X),State)
| -differ(X,Z).

% ---- putdown rules -----
%
% Similarly to picking up a block, what is required for putting it down
% and what happens to the state after putting down.
%
% The first rule states that the robot hand will be empty after
% it puts down something
%
% ---------------------

holds(empty,do(putdown(X,Y),State))
| -holds(holding(X),State)
| -holds(clear(Y),State).

holds(on(X,Y),do(putdown(X,Y),State))
| -holds(holding(X),State)
| -holds(clear(Y),State).

holds(clear(X),do(putdown(X,Y),State))
| -holds(holding(X),State)
| -holds(clear(Y),State).

% ---- frame axioms for putdown -----

holds(on(X,Y),do(putdown(Z,W),State))
| -holds(on(X,Y),State).

holds(clear(Z),do(putdown(X,Y),State))
| -holds(clear(Z),State)
| -differ(Z,Y).

% ----- queries -----------------
%
% first run the uncommented query and then:
%
% * try out the others: uncomment one and comment out others
% * create your own goals: see what can be achieved in sensible time and what not.
%
% Solving queries in the block world is surprisingly hard:
% there are lot of possible action paths the robot hand could take
% and there are a lot of axioms which have to be checked and used.
%
% If you wanted to do real planning quickly in a formalization like this,
% you'd need a specialized search strategy plus possibly special mechanisms
% for ignoring some potential paths of actions and some sequences of
% derivations from rules: it nthis way the search could be made fast.
% The default search strategies of provers are pretty bad for these
% kinds of problems.
%
% -------------------------------

% first goal: try to put "b" on "a".
%
%  b
%  a
%
% Notice we do not require that "a" is on "table": it could
% well be sitting on a block "c".

% this version simply asks whether a sequence of required moves
% exists but does not explicitly print it out as an answer:
%
% -holds(on(b,a),State).

% this version gives the required moves collected into State,
% as required for planning the actions:

-holds(on(b,a),State) | \$ans(State).

% second goal:
%
%  c
%  b
%  a

% -holds(on(b,a),State) | -holds(on(c,b),State).
%
% this version gives the required moves collected into State (over a minute to find proof!)
%
%
% cnf(prove,negated_conjecture,
%   -holds(on(b,a),State) | -holds(on(c,b),State) | \$ans(State)).

```