Existence, Uniqueness, and Construction of Rewrite Systems
Nachum Dershowitz, Leo Marcus, Andrzej Tarlecki · SIAM Journal on Computing · 1988
The construction of term-rewriting systems, specifically by the Knuth–Bendix completion procedure, is considered. We look for conditions that might ensure the existence of a finite canonical rewriting system for a given equational theory and that might guarantee that the completion procedure will find it. We define several notions of equivalence between rewriting systems in the ordinary and modulo case, and examine uniqueness of systems and the need for backtracking in implementing completion.