procédure de complétion

CONT: A completion procedure is a way to generate a rewrite system without such divergent critical pairs with the same proving power. It is based on inference rules like the following ones where one works on a data structure with two sets, namely E that contains the identities and R that contains the rules or oriented identities.