zbMATH — the first resource for mathematics

Confluence as a cut elimination property. (English) Zbl 1038.03054
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].

03F05 Cut-elimination and normal-form theorems
68Q42 Grammars and rewriting systems
Full Text: Link