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.

翻译：我们证明，即使底层理论是可判定的，可终止的局部约束重写系统的（局部）汇合性也是不可判定的。已有若干针对逻辑约束重写系统的汇合性判定准则。这些准则是通过在约束环境下重述普通项重写系统的既有证明而获得的，涉及非平凡的工作。我们提出一种从逻辑约束重写系统到项重写系统的简单变换，使得后者的临界对对应于前者的约束临界对。该变换的有效性通过将基于（几乎）发展封闭临界对以及并行临界对的先进汇合性结果提升至约束环境而得到验证。