Un article de Wikipédia, l'encyclopédie libre.
La procédure de complétion de Knuth-Bendix transforme un ensemble d'identités (sur des termes) décrivant une structure algébrique en un système de réécriture de terme confluent et qui termine (dit alors convergent). Quand cette procédure se termine en produisant un système de réécriture convergent, elle donne un moyen effectif de résoudre le problème du mot pour l'algèbre en question. Le problème du mot étant indécidable en général, la procédure ne se termine pas toujours avec succès. Elle peut soit s'exécuter indéfiniment, soit échouer en rencontrant une identité non-orientable (qu'elle ne peut pas transformer en règle de réécriture sans être sure de ne pas mettre en danger la terminaison).
Il existe une procédure de complétion améliorée qui n'échoue pas sur les identités non orientables. Elle fournit une procédure de semi-décision pour le problème du mot, autrement dit, elle permet de dire si une identité donnée est déductible des identités qui décrivent l'algèbre en question.
