Sets of equations E play an important computational role in rewriting-based systems R by defining an equivalence relation =E inducing a partition of terms into E-equivalence classes on which rewriting computations, denoted ->R/E and called *rewriting modulo E*, are issued. This paper investigates *confluence of ->R/E*, usually called *E-confluence*, for *conditional* rewriting-based systems, where rewriting steps are determined by conditional rules. We rely on Jouannaud and Kirchner's framework to investigate confluence of an abstract relation R modulo an abstract equivalence relation E on a set A. We show how to particularize the framework to be used with conditional systems. Then, we show how to define appropriate finite sets of *conditional pairs* to prove and disprove E-confluence. In particular, we introduce *Logic-based Conditional Critical Pairs* which do not require the use of (often infinitely many) E-unifiers to provide a finite representation of the *local peaks* considered in the abstract framework. We also introduce *parametric Conditional Variable Pairs* which are essential to deal with conditional rules in the analysis of E-confluence. Our results apply to well-known classes of rewriting-based systems. In particular, to *Equational (Conditional) Term Rewriting Systems*. In this realm, our E-confluence results strictly subsume previous approaches by Huet and Jouannaud and Kirchner.

翻译：在基于重写的系统R中，方程集E通过定义等价关系=E起着重要的计算作用，该关系将项划分为E等价类，在这些类上执行重写计算（记为->R/E，称为*模E重写*）。本文研究*条件*基于重写的系统中->R/E的*合流性*（通常称为*E合流性*），其中重写步骤由条件规则决定。我们依据Jouannaud和Kirchner的框架，研究集合A上抽象关系R模抽象等价关系E的合流性。我们展示了如何将该框架特化以用于条件系统。接着，我们展示了如何定义适当的有限*条件对*集合来证明和证伪E合流性。特别地，我们引入了*基于逻辑的条件临界对*，它无需使用（通常无限多的）E合一子即可为抽象框架中考虑的*局部峰*提供有限表示。我们还引入了*参数化条件变量对*，这对处理E合流性分析中的条件规则至关重要。我们的结果适用于已知的基于重写的系统类别，特别是*方程（条件）项重写系统*。在此领域中，我们的E合流性结果严格包含了Huet以及Jouannaud和Kirchner先前的方法。