Normalized Rewriting: an unified view of Knuth-Bendix completion and Gröbner bases computation

Abstract

Buchberger's algorithm and Knuth-Bendix completion are two fundamental algorithms used respectively in computer algebra and in equational logic. It has been remarked since 1981 that these two algorithms behave in the same way. We show that this similarity is made explicit by viewing them as two particular instances of a very general completion algorithm: normalized completion.

full paper