クヌース・ベンディックス完備化アルゴリズム
グレブナー基底は、多変数多項式の簡約化を一意に行える多項式の集合であり、グレブナー基底を求めるブッフベルガーアルゴリズムは数式処理の分野での連立代数方程式の解法や、可換環論、代数幾何、微分方程式論、整数計画問題などに出てくる様々な数学的対象物を構成するための基礎となっている。
クヌース・ベンディックス完備化アルゴリズムでの危険対はブッフベルガーアルゴリズムでのS-多項式、項順序は単項式順序に対応する。
具体例として群の公理を完備化する。群の公理は以下の通り。
1. 0 + a = a
2. (-a) + a = 0
3. (a + b) + c = a + (b + c)
完備化アルゴリズムは以下のように行う。
4. ((-a) + a) + b ... 2と3より生成 = 0 + b = b ... 2、次に、1より = (-a) + (a + b) ... 3より (-a) + (a + b) の方が式として大きいので、(-a) + (a + b) = b を追加。
5. (-0) + (0 + a) ... 1と4より生成 = (-0) + a ... 1より = a ... 4より (-0) + a の方が式として大きいので、(-0) + a = a を追加。
6. (-(-a)) + ((-a) + a) ... 2と4より生成 = (-(-a)) + 0 ... 2より = a ... 4より (-(-a)) + 0 の方が式として大きいので、(-(-a)) + 0 = a を追加。
このような作業を数十回繰り返し、冗長な物を取り除くと、最終的にこの式が残る。
0 + a = a
(-a) + a = 0
(a + b) + c = a + (b + c)
(-a) + (a + b) = b
a + 0 = a
a + (-a) = 0
a + ((-a) + b) = b
-0 = 0
-(-a) = a
-(b + a) = (-a) + (-b)