% 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 assumption              : (true => re(a,b),re(a,c)).
_ axiom goal_axiom(X)           : (re(b,X),re(c,X) => goal).

% equality axioms
_ axiom reflexivity_of_e(X)     : (dom(X) => e(X,X)).
_ axiom symmetry_of_e(X,Y)      : (e(X,Y) => e(Y,X)).
_ axiom left_congr_of_e(X,Y,Z)  : (e(X,Y),re(Y,Z) => re(X,Z)).

% basic facts on re
_ axiom re_contains_e(X,Y)      : (e(X,Y) => re(X,Y)).
_ axiom re_contains_r(X,Y)      : (r(X,Y) => re(X,Y)).
_ axiom re_elimination(X,Y)     : (re(X,Y) => e(X,Y);r(X,Y)).

% DP
_ axiom diam_prop_of_r(X,Y,Z)   : (r(X,Y),r(X,Z) => dom(U),r(Y,U),r(Z,U)).