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