Proper noun
Knuth-Bendix completion algorithm (computing theory) A semidecision algorithm for transforming a set of equations (over terms) into a confluent term rewriting system.