Confluence as a cut elimination property. (English) Zbl 1038.03054

Dowek, Gilles

Nieuwenhuis, Robert (ed.), Rewriting techniques and applications. 14th international conference, RTA 2003, Valencia, Spain, June 9–11, 2003. Proceedings. Berlin: Springer (ISBN 3-540-40254-3/pbk). Lect. Notes Comput. Sci. 2706, 2-13 (2003).

Summary: 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.
For the entire collection see [Zbl 1029.00060].

MSC:

03F05	Cut-elimination and normal-form theorems
68Q42	Grammars and rewriting systems

Keywords:

confluence; cut elimination; asymmetric deduction; rewriting system on terms