Confluence of Conditional Rewriting Modulo

We investigate confluence of rewriting with Equational Generalized Term Rewriting Systems R, consisting of Horn clauses, some of them defining conditional equations s = t double left arrow c and rewriting rules l -> r double left arrow c. In both cases, c is a sequence of atoms, possibly defined by using additional Horn clauses. Such systems include Equational Term Rewriting Systems and (join, oriented, and semi-equational) Conditional Term Rewriting Systems. A set of equations E defines an equivalence = E and quotient set T (F, X)/= E of terms, where reductions s ->(R/E) t using rules in R occur. For such systems, we obtain a finite set of conditional pairs pi, which can be viewed as logical sentences, to prove and disprove confluence of ->(R/E) by (dis)proving joinability of such conditional pairs pi.