% DELAYING META-INTERPRETER
% CILog code. Copyright David Poole, 1997.

% dprove(G,D0,D1) is true if G can be proven from the delayables in D1-D0
%   where D0 is a tail of D1.

%% Intuitively, D0 are the assumptions made before G, and D1 are the
%% assumptions made after G. D1 consists of D0 and the assumptions
%% needed to prove G.

dprove(true,D,D).
dprove((A & B),D1,D3) <-
   dprove(A,D1,D2) &
   dprove(B,D2,D3).
dprove(G,D,[G|D]) <-
   delay(G).
dprove(H,D1,D2) <-
   (H <= B) &
   dprove(B,D1,D2).