Complétion Knuth–Bendix

Procédure appliquée à un système de réécriture présenté qui tente de produire un système de réécriture confluent (complet) en orientant les relations en règles de réécriture selon un ordre de réduction choisi et en ajoutant les conséquences issues des recouvrements critiques jusqu'à ce qu'il ne reste plus de paires critiques non résolues ou que le processus diverge.

Une procédure algorithmique qui prend un ensemble de règles de réécriture (ou de relations) et un ordre de réduction bien fondé, puis tente d'étendre l'ensemble de règles en ajoutant des conséquences (résolution des paires critiques) afin d'obtenir un système de réécriture confluent (et terminé) qui résout le problème des mots pour l'algèbre présentée lorsque la procédure aboutit.