Knuth-Bendix Completion Algorithm

Um algoritmo usado em álgebra computacional para transformar um conjunto de equações em um sistema de reescrita de termos confluente, permitindo a verificação de igualdades em uma teoria equacional.