CS322, Fall 1997 - Practice Final -- Solution to Question 6

Go up to Question 6

Solution to Question 6

reduce_prove(L_0,L_1) <-
    reduce_prove_acc(L_0,[],L_1).

reduce_prove_acc(L₀,A₀,A₁) is true if starting with primitives A₀ also proving the elements of L₀ results in primitives A₁.

reduce_prove_acc([],L,L).
reduce_prove_acc([true|R],A_0,A_1) <-
    reduce_prove_acc(R,A_0,A_1).
reduce_prove_acc([P|R],A_0,A_1) <-
    primitive(P)&
    reduce_prove_acc(R,[P|A_0],A_1).
reduce_prove_acc([A& B|R],A_0,A_1) <-
    reduce_prove_acc([A,B|R],A_0,A_1).
reduce_prove_acc([H|R],A_0,A_1) <-
    (H <= B)&
    reduce_prove_acc([B|R],A_0,A_1).