%  A Blocks World Problem with Incomplete Initial Situation

/* Initial situation: Only the blocks so indicated have been
   specified to be clear.
                               d
        clear --> p            a          m <--- clear; not on table
 not on table --> n            .
                            ? . . ?           f <--- not on table
                             .   .
                     g      b     .
                     h      c      e     k
                  --------------------------

Goal situation              d     k
                            h     g
                            b     m
                            e     f
                            a     c
                          -----------                     */

goal(S) :- prove( on(d,h,S) & on(h,b,S) & on(b,e,S) & on(e,a,S) &
           ontable(a,S) & on(k,g,S) & on(g,m,S) & on(m,f,S) &
           on(f,c,S) & ontable(c,S) ).

goodTower(X,S) <=> X = a & ontable(a,S) v
    X = e & on(e,a,S) & ontable(a,S) v
    X = b & on(b,e,S) & on(e,a,S) & ontable(a,S) v
    X = h & on(h,b,S) & on(b,e,S) & on(e,a,S) & ontable(a,S) v
    X = d & on(d,h,S) & on(h,b,S) & on(b,e,S) & on(e,a,S) & ontable(a,S) v
    X = c & ontable(c,S) v
    X = f & on(f,c,S) & ontable(c,S) v
    X = m & on(m,f,S) & on(f,c,S) & ontable(c,S) v
    X = g & on(g,m,S) & on(m,f,S) & on(f,c,S) & ontable(c,S) v
    X = k & on(k,g,S) & on(g,m,S) & on(m,f,S) & on(f,c,S) & ontable(c,S).

/*  Initial database. Notice that all references to clear and ontable
    have been eliminated, via their definitions, in favour of on. This
    considerably improves the efficiency of prime implicate generation. */

axiom(all([y,block],-on(y,m,s0))).               % m is clear.
axiom(all([y,block],-on(y,p,s0))).               % p is clear.
axiom(all([x,block],-on(k,x,s0))).               % k is on the table.
axiom(all([x,block],-on(c,x,s0))).               % c is on the table.
axiom(all([x,block],-on(e,x,s0))).               % e is on the table.
axiom(all([x,block],-on(h,x,s0))).               % h is on the table.
axiom(on(b,c,s0)).   axiom(on(d,a,s0)).
axiom(on(g,h,s0)).   axiom(on(p,n,s0)).
axiom(on(a,b,s0) v on(a,e,s0)).                  % a is on b or on e,
axiom(all([x,block],on(x,b,s0) => x = a)).       % and no other block
axiom(all([x,block],on(x,e,s0) => x = a)).       % is on b or on e.
axiom(some([x,block],on(f,x,s0))).               % f is not on the table.
axiom(some([x,block],on(m,x,s0))).               % m is not on the table.
axiom(some([x,block],on(n,x,s0))).               % n is not on the table.
axiom(all([x,block],all([y,block], on(x,y,s0) => -on(y,x,s0)))).
axiom(all([x,block],all([y,block], all([z,block],
               on(y,x,s0) & on(z,x,s0) => y = z)))).
axiom(all([x,block],all([y,block], all([z,block],
               on(x,y,s0) & on(x,z,s0) => y = z)))).

/*  clear and ontable defined in the initial situation. This is
    needed by the regression theorem-prover to eliminate clear
    and ontable in favour of on in regressed formulas.  */

clear(X,s0) <=> all([y,block],-on(y,X,s0)).
ontable(X,s0) <=> all([y,block],-on(X,y,s0)).

%  Domain of individuals.

domain(block, [a,b,c,d,e,f,g,h,k,m,n,p]).

%  Action preconditions.

poss(move(X,Y),S) :- domain(block,D),
                     findall(Z,(member(Z,D), prove(clear(Z,S))),L),
                     member(X,L), member(Y,L), not X = Y.
poss(moveToTable(X),S) :- domain(block,D), member(X,D),
                          prove(clear(X,S) & -ontable(X,S)).

/* Successor state axioms instantiated by action terms to
   simplify implementation of the regression theorem-prover. */

clear(X,do(move(U,V),S)) <=> on(U,X,S) v -(X = V) & clear(X,S).
clear(X,do(moveToTable(U),S)) <=> on(U,X,S) v clear(X,S).

on(X,Y,do(move(U,V),S)) <=> X = U & Y = V v -(X = U) & on(X,Y,S).
on(X,Y,do(moveToTable(U),S)) <=> -(X = U) & on(X,Y,S).

ontable(X,do(move(U,V),S)) <=> -(X = U) & ontable(X,S).
ontable(X,do(moveToTable(U),S)) <=> X = U v ontable(X,S).

primitive_action(move(X,Y)).   primitive_action(moveToTable(X)).