クヌース・ベンディックス完備化アルゴリズム（）、あるいはクヌース・ベンディックス完備化手続きは、等式の有限集合をそれと等価な完備性のある項書き換えシステムに変換するアルゴリズムである。このアルゴリズムは普遍代数（）での"語の問題"（）（）を解くための手法としてクヌースとベンディックスから提案された。アルゴリズムは必ず成功するとは限らないが、成功した場合は停止性と合流性のある項書き換えシステムを生成することができる。そのベースとなる考え方は多くの分野で応用することができる。一般に、項書き換えシステムは項の書き換え（"簡約"、）が必ず停止するとは限らず、また書き換えの際に複数の書き換え規則を適用できる場合は最終的な結果が一意になるとは限らない。無限の簡約の列が存在しないことを"停止性"、複数の書き換え規則を適用可能な場合にその後の簡約の流れが合流することを"合流性"と言う。停止性と合流性を両方もっていれば、システムは完備（）と言う。完備性があるシステムは、最終的な結果が必ず求まり、その結果は簡約の順序によらず一意になる。以下では、"a" から "b" への簡約を formula_1 、"a" を簡約していってこれ以上簡約できなくなった最も単純な形（"正規形"、）を formula_2 と表記する。ある要素に対し2つの書き換え規則を適用可能な場合がありうる。2つの規則の条件に重なりがあるとき、それらの規則で簡約した異なる結果のペアを危険対（）と呼ぶ。危険対が存在する場合、どの書き換え規則を適用するかにより簡約の結果が変わる可能性がある。例えば、以下の項書き換え規則を考える。項 formula_5 を考える。 ρ を適用すると項 formula_6 が得られ、ρ を適用すると項 formula_7 が得られる。このときの危険対は、formula_8 である。危険対の要素をそれぞれ簡約化して正規形を求めたとき、両者が一致する場合を"収束する"、一致しない場合を"発散する"という。危険対について、以下の定理が成立する。書き換え規則が有限であれば危険対も有限であり、項書き換えシステムが停止性をみたす場合は危険対の各要素の正規形も有限の簡約ステップで求めることができる。つまり、停止性を満たす項書き換えシステムの合流性は以下の有限のステップで分かる。クヌース・ベンディックス完備化アルゴリズムは等式の有限集合をそれと等価な完備性のある項書き換えシステムに変換する。等式の有限集合とは、例えば以下の formula_14 ようなものである。これは群の公理である単位元の存在、逆元の存在、結合法則を表す。これらより formula_16, formula_17, formula_18 のような項書き換えの規則 formula_19 を作成する。特定の等式 formula_20 が成立するかどうかを調べるためには、"u

出典:wikipedia