Numerous confluence criteria for plain term rewrite systems are known. For logically constrained rewrite system, an attractive extension of term rewriting in which rules are equipped with logical constraints, much less is known. In this paper we extend the strongly-closed and (almost) parallel-closed critical pair criteria of Huet and Toyama to the logically constrained setting. We discuss the challenges for automation and present crest, a new tool for logically constrained rewriting in which the confluence criteria are implemented, together with experimental data.

翻译：针对无约束项重写系统，已有诸多合流准则被提出。而逻辑约束重写系统作为项重写的一种富有吸引力的扩展——其中的规则配备了逻辑约束——对此类系统的研究则相对匮乏。本文我们将Huet与Toyama提出的强封闭与（几乎）平行封闭关键对准则扩展至逻辑约束框架。我们探讨了自动化实现的挑战，并介绍了实现上述合流准则的新型逻辑约束重写工具crest，同时给出了实验数据。