The goal of this note is to compare two notions, one coming from the theory of rewrite systems and the other from proof theory: confluence and cut elimination. We show that to each rewrite system on terms, we can associate a logical system: asymmetric deduction modulo this rewrite system and that the confluence property of the rewrite system is equivalent to the cut elimination property of the associated logical system. This equivalence, however, does not extend to rewrite systems directly rewriting atomic propositions.

翻译：本文旨在比较两个概念，一个来自重写系统理论，另一个来自证明论：合流性与切消除。我们证明，对于项上的每个重写系统，可以关联一个逻辑系统：基于该重写系统的不对称演绎模系统，并且该重写系统的合流性等价于关联逻辑系统的切消除性质。然而，这种等价性并不直接扩展至重写原子命题的重写系统。