Proof-theoretic techniques for term rewriting theory

A bridge is presented between term-rewriting theory in computer science and proof theory in logic. It is shown that proof-theoretic tools are very useful for analyzing two basic attributes of term rewriting systems, the termination property and the Church-Rosser property. A counterexample is given to show that Knuth´s critical pair lemma does not hold for conditional rewrite systems. Two restrictions on conditional systems under which the critical pair lemma holds are presented. One is considered a generalization of Bergstra-Klop´s former result; the other is concerned with a generalization of Kaplan´s and Jouannaud-Waldmann´s systems.<>