% DP(r) => DP(re), i.e., % the diamond property is preserved under reflexive closure name(dpe). :- dynamic e/2,r/2,re/2. % domain elements a,b,c dom(a). dom(b). dom(c). _ axiom assump : (true => re(a,b),re(a,c)). _ axiom goal_ax(X): (re(b,X),re(c,X) => goal). % equality axioms _ axiom ref_e(X) :(dom(X) => e(X,X)). _ axiom sym_e(X,Y) :(e(X,Y) => e(Y,X)). _ axiom congl(X,Y,Z) :(e(X,Y),re(Y,Z) => re(X,Z)). % basic facts on re _ axiom e_in_re(X,Y) :(e(X,Y) => re(X,Y)). _ axiom r_in_re(X,Y) :(r(X,Y) => re(X,Y)). _ axiom e_or_r(X,Y) :(re(X,Y) => e(X,Y);r(X,Y)). % DP _ axiom dp_r(X,Y,Z) :(r(X,Y),r(X,Z) => dom(U),r(Y,U),r(Z,U)).