CS322, Fall 1997 - Practice Final -- Answer to Question 1, part 2

Go backward to Answer to Question 1, part 1
Go up to Question 1
Go forward to Answer to question 1, extra question

Answer to Question 1, part 2

Give an SLD-resolution showing how how a delaying meta-interpreter can be used to find one of these minimal conflicts.

Consider the delaying meta-interpreter where dprove(G,D₀,D₁) is true if D₀ is an ending of D₁ and G logically follows from the conjunction of the assumable atoms in D₁.

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

The following shows an SLD resolution to find conflicts:

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