%--------------------------------------------------------------% 
%   Situation Calculus (simple deductive planning)             % 
%   by using depth-bound strategy                              % 
%   (C) 1998 Zdravko Markov                                    % %--------------------------------------------------------------%  
% Sample queries 
% ?- holds(on(a,c),S,1). 
% no 
% ?- holds(on(a,c),S,2). 
% no 
% ?- holds(on(a,c),S,3). 
% S = [puton(a,c),puton(b,table),puton(a,table)] ? 
% 
% ?- holds((on(b,a),on(c,b)),S,3). 
% S = [puton(c,b),puton(b,a),puton(a,table)] ?   
%--------------------------------------------------------------- 
% holds(+Goals,-Situation,+Steps).  

% Initial Situation 
holds(on(a,b),[],_):-write('init state 1'),nl. 
holds(on(b,c),[],_):-write('init state 2'),nl. 
holds(clear(a),[],_):-write('init state 3'),nl. 
holds(on(c,table),[],_):-write('init state 4'),nl.  

% Axioms 
holds(on(A,B),[puton(A,B)|S],N) :- write('axiom 1'),nl,
      N>0, M is N-1,
     neq(A,B),
write(neq(A,B)),nl,
     holds(clear(A),S,M),
     write(clear(A)),tab(5),write(s=S),tab(4),write(m=M),nl,
     holds(clear(B),S,M). 

holds(clear(C),[puton(A,B)|S],N) :- write('axiom 2'),nl,
    N>0, M is N-1,
     neq(A,B),
write(neq(A,B)),nl,
     holds(on(A,C),S,M),
     write(on(A,C)),tab(5),write(s=S),tab(4),write(m=M),nl,
     holds(clear(A),S,M),
     write(clear(A)),tab(5),write(s=S),tab(4),write(m=M),nl,
     holds(clear(B),S,M).  

% Frame Axioms 
holds(on(X,Y),[puton(A,B)|S],N) :-write('frame axiom 1'),nl,
     N>0, M is N-1,
     neq(A,B), 
write(new(A,B)),nl,
    neq(A,X), 
write(new(A,X)),nl,
    neq(B,Y), 
write(new(B,Y)),nl,
    holds(on(X,Y),S,M). 

holds(clear(X),[puton(_,B)|S],N) :-write('frame axiom 2'),nl,
     N>0, M is N-1,
     neq(X,B),
write(new(X,B)),nl,
     holds(clear(X),S,M). 
holds(clear(table),S,_):-write('frame axiom 3'),nl,write(s=S),nl.  

% Solving conjunctive goals 
holds((A,B),S,N) :-
    holds(A,S,N),
    holds(B,S,N).  

% Extensional definition of not equal 

neq(a,table). 
neq(table,a). 
neq(b,table). 
neq(table,b). 
neq(c,table). 
neq(table,c). 
neq(a,b). 
neq(a,c). 
neq(b,a). 
neq(c,a). 
neq(b,c).
 neq(c,b).