Blocks world axiom/query examples from lecture

First, a simple version.

%set(auto).
set(factor).
set(binary_res).

%clear(print_kept).

set(prolog_style_variables).

list(sos).
%formulas(sos).

% ----- initial situation ------


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


% ---- rules -----


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

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

% ----- query -------

end_of_list.

list(usable).


-holds(on(b,a),State) | -holds(on(c,b),State).


%-holds(and(on(c,b),on(b,a)),State).
  


end_of_list.    

Second, a lot more complex version (not necessarily better!)

% this is the way comments start
%set(hyper_res).  % another alternative is set(binary_res)
%set(factor).   % probably comes automatically
%set(para_from).
%set(para_into).
set(auto).
clear(print_kept).  % this will print out ALL derived and kept stuff

%formula_list(sos).  % use list(sos) if not formula syntax
formulas(sos).

on(b,table,s0).
on(a,table,s0).
on(c,table,s0).
empty(s0).
all x hasspace(table,x).


-on(b,a,s0).
-on(a,b,s0).
-on(c,b,s0).
-on(c,a,s0).
-on(a,c,s0).
-on(b,c,s0).
all x all y -on(table,x,y).

block(a).
block(b).
block(c).
-block(table).


% being clear: closed world

all z ((-on(b,a,z) & -on(c,a,z))  ->  clear(a,z)).
all z ((-on(a,b,z) & -on(c,b,z))  ->  clear(b,z)).    
all z ((-on(a,c,z) & -on(b,c,z))  ->  clear(c,z)).
    
% general world rules

all x all y (clear(x,y) -> hasspace(x,y)).

all x all y all z 
   ((on(x,y,z) & block(y))
     -> 
     -on(x,table,z)).
          
all x all z 
   ( -(exists y on(y,x,z))
     -> 
     clear(x,z)).       

% closed world

%all x (x=a | x=b | x=c | x=table).
%a!=b.
%a!=c.
%a!=table.
%b!=c.
%b!=table.
%c!=table.

all x (sameas(x,a) | sameas(x,b) | sameas(x,c) | sameas(x,table)).
-sameas(a,b).
-sameas(a,c).
-sameas(a,table).
-sameas(b,c).
-sameas(b,table).
-sameas(c,table).

all x sameas(x,x).
all x all y (sameas(x,y) -> sameas(y,x)).
%all x all y all z (sameas(x,y) & sameas(y,z) -> sameas(x,z)).



% actions

all x all y all z 
   ((holds(x,z) &
     hasspace(y,z) &
     -sameas(x,y) )
     -> 
    (on(x,y,puton(x,y,z)) &        
     -clear(y,puton(x,y,z)) &           
     clear(x,puton(x,y,z)) &               
     hasspace(x,puton(x,y,z)) &
     empty(puton(x,y,z))) ).        
      
    
all x all y all z 
   ((on(x,y,z) &
     empty(z) &
     clear(x,z))
     -> 
    (-on(x,y,lift(x,z)) & 
     clear(y,lift(x,z)) &
     hasspace(y,lift(x,z)) &
     holds(x,lift(x,z))) ).
     

% frame axioms

all x all y all z 
   (-on(x,y,z) 
     -> 
    -on(x,y,lift(x,z)) ).
    
all x all y all z all u 
   ((on(x,y,z) & -sameas(u,x))
     -> 
    on(x,y,lift(u,z)) ).    
    
all x all y all z 
   ((clear(x,z) & -sameas(x,y))  
     -> 
    clear(x,lift(y,z)) ).     

all x all y all z 
   ((-clear(x,z) & -on(y,x))
     -> 
    -clear(x,lift(y,z)) ).

% 

all x all y all z all u
   (-on(x,y,z) 
     -> 
    -on(x,y,puton(x,z)) ).
    
all x all y all z all u 
   ((on(x,y,z) & -sameas(u,x))
     -> 
    on(x,y,lift(u,z)) ).    
    
all x all y all z all u
   ((clear(x,z) & -sameas(x,y))  
     -> 
    clear(x,puton(u,y,z)) ).     

all x all y all z all u
   ((-clear(x,z) & -sameas(u,x))
     -> 
    -clear(x,puton(u,y,z)) ).

% queries


all z ((on(c,a,z) & on(b,c,z))  -> $answer(z)).
%all z (on(b,c,z)   -> $answer(z)).
%all z (on(c,a,z)   -> $answer(z)).
%all z (clear(a,z) -> $answer(z)).


end_of_list.