# original version at http://www.ii.uib.no/~bezem/GL/dpe.in
# DP(r) => DP(re), i.e. the diamond property is preserved under reflexive closure

@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <dpe#>.

:a :re :b.
:a :re :c.

# equality axioms
{?X :re ?Y} => {?X :e ?X}.
{?X :re ?Y} => {?Y :e ?Y}.

{?X :e ?Y} => {?Y :e ?X}.
{?Y :not_e ?X} => {?X :not_e ?Y}.

{?X :not_re ?Z. ?Y :re ?Z} => {?X :not_e ?Y}.
{?X :e ?Y. ?X :not_re ?Z} => {?Y :not_e ?Z}.

# basic facts on re
{?X :e ?Y} => {?X :re ?Y}.
{?X :r ?Y} => {?X :re ?Y}.

{?X :re ?Y. ?X :not_e ?Y} => {?X :r ?Y}.
{?X :re ?Y. ?X :not_r ?Y} => {?X :e ?Y}.

# DP
{?X :r ?Y. ?X :r ?Z} => {?Y :r ?U. ?Z :r ?U}.

# assuming the negation of the query so that it can be discharged when the query succeeds
{:b :re ?X} => {:c :not_re ?X}.
{:c :re ?X} => {:b :not_re ?X}.
