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.

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