Consider the delaying meta-interpreter where dprove(G,D0,D1) is true if D0 is an ending of D1 and G logically follows from the conjunction of the assumable atoms in D1.
The following shows an SLD resolution to find conflicts:dprove(true,D,D). dprove((A& B),D_1,D_3)<- dprove(A,D_1,D_2)& dprove(B,D_2,D_3). dprove(G,D,[G|D])<- assumable(G)& notin(G,D). dprove(G,D,D)<- assumable(G)& member(G,D). dprove(H,D_1,D_2)<- (H<= B)& dprove(B,D_1,D_2).
yes(D) <- dprove(false,[],D). yes(D) <- (false <= B_1) & dprove(B_1,[],D). yes(D) <- dprove((a & b),[],D). yes(D) <- dprove(a,[],D_1)& dprove(b,D_1,D). yes(D) <- (a <= B_2) & dprove(B_2,[],D_1)& dprove(b,D_1,D). yes(D) <- dprove(p,[],D_1)& dprove(b,D_1,D). yes(D) <- dprove(p,[],D_1)& dprove(b,D_1,D). yes(D) <- assumable(p) & notin(p,[]) & dprove(b,[p],D). yes(D) <- notin(p,[]) & dprove(b,[p],D). yes(D) <- dprove(b,[p],D). yes(D) <- (b <= B_3) & dprove(B_3,[p],D). yes(D) <- dprove(e,[p],D). yes(D) <- (e <= B_4) & dprove(B_4,[p],D). yes(D) <- dprove(p,[p],D). yes([p]) <- assumable(p) & member(p,[p]). yes([p]) <- member(p,[p]). yes([p]) <- .