We show that (local) confluence of terminating locally constrained rewrite systems is undecidable, even when the underlying theory is decidable. Several confluence criteria for logically constrained rewrite systems are known. These were obtained by replaying existing proofs for plain term rewrite systems in a constrained setting, involving a non-trivial effort. We present a simple transformation from logically constrained rewrite systems to term rewrite systems such that critical pairs of the latter correspond to constrained critical pairs of the former. The usefulness of the transformation is illustrated by lifting the advanced confluence results based on (almost) development closed critical pairs as well as on parallel critical pairs to the constrained setting.

翻译：我们证明，终止的局部约束重写系统的（局部）合流性不可判定，即使底层理论是可判定的。已知逻辑约束重写系统存在若干合流性判据，这些判据通过将普通项重写系统的现有证明在约束场景下重新演绎获得，涉及大量工作。本文提出一种从逻辑约束重写系统到项重写系统的简单变换，使得后者的临界对对应于前者的约束临界对。通过将基于（几乎）发展封闭临界对以及平行临界对的高级合流性结果提升至约束场景，验证了该变换的有效性。