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