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