クヌース・ベンディックス完備化アルゴリズム

3行要約

1. 項書き換え系において、与えられた等式の集合を完備な書き換え系に変形する手法。
2. 合流性と停止性を備えることで、項の等価性を効率的に判定可能にする。
3. 自動定理証明や数式処理システムの最適化などに広く応用されている。