Simple axiomatization of the blocks world

% ----- initial situation s0 ------
%
%           c 
%   a   b   d
%  ------------------------------

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

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

%holds(and(X,Y),State) 
%    | -holds(X,State)
%    | -holds(Y,State).

% ----- pickup rules  ------

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

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

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

% ---- a few minimal 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.
%
% ------------------------------- 

% first goal:
%
%  b
%  a

% -holds(on(b,a),State).
%
% this version gives the required moves collected into State:
%

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