Conflunt reductions: Abstract properties and applications to term rewriting systems

This paper gives new results, and presents old ones in a unified formalism, concerning Church-Rosser theorems for rewriting systems, and shows how these results yield efficient methods for the mechanization of equational theories.

Abstract

This paper gives new results, and presents old ones in a unified formalism, concerning Church-Rosser theorems for rewriting systems. Part 1 gives abstract confluence properties, depending solely on axioms for a binary relation called reduction. Results of Newman and others are presented in a unified formalism. Systematic use of a powerful induction principle permits to generalize results of Sethi on reduction modulo equivalence. Part 2 concerns simplification systems operating on terms of a first-order logic. Results by Rosen and Knuth and Bendix are extended to give several new criteria for confluence of these systems, using the results of part 1. It is then shown how these results yield efficient methods for the mechanization of equational theories.