We define a new kind of rewriting which generalizes the known notion of rewriting modulo an equational theory. This rewrite relation allows us to rewrite modulo theories for which the previous notion was not applicable, including identity, idempotency, Abelian group theory and commutative ring theory. We obtain a new completion algorithm which contains as an instance the usual Knuth-Bendix completion algorithm, but also algorithms for computing standard bases of polynomial ideals, of Buchberger, and Kandri-Rody and Kapur.
We investigate the particular case of completion of ground equations, and we prove by a uniform method the termination of the completion process for a interesting class of theories, generalizing the result of Narendran and Rusinowitch for ground equations modulo AC, and the result of Buchberger and the one of Kandri-Rody and Kapur for polynomial ideals.
We obtain then decidability results on the word problem for some classes of equational theories, including the AC-ground case (already obtained by Narendran and Rusinowitch), the AC1I-ground case (a new result to our knowledge), and the cases of ground theories modulo the theory of Abelian groups and commutative rings, which is already known in the case when the signature contains only constants, but is new if not.
We have also a result of undecidability for the word problem in a case between AC and rings, the ACD-ground case, also a new result to our knowledge.
Finally, we have an implementation which shows the efficiency of normalized completion with respect to completion modulo AC.