Knuth-Bendix 完备化算法

Knuth-Bendix 完备化算法尝试将有限的 恒等式 集合转换为一个 有限终止、合流 的 项重写系统，其归约保持恒等性。这个项重写系统充当验证恒等式的判定程序。

正如在 泛代数 中定义的，恒等式是两个 项 的等式: 。据推测，对于其中出现的所有变量的值，这两个项的值都相等。 归约序 是完备化算法的另一个输入，前提是将每个恒等式视为将左侧转换为右侧，反之亦然的重写规则的两个候选者。

输出的 项重写系统 用于确定 是否是恒等式，方法如下。如果两个不同的项 和 具有相同的范式，则 是恒等式。否则， 不是恒等式。既是 有限终止 又是 合流 的项重写系统享有对所有表达式都具有唯一范式的性质。 决定 是否是恒等式的问题也称为词问题。

最初，该算法尝试根据归约序定向输入恒等式 (如果 ，则 成为规则)。 然后，它用导出的规则完成这组初始规则。 该算法迭代地检测 临界对，获得它们的范式，并根据 归约序 为每对范式添加新规则。

该算法可能

1. 成功终止并产生一个有限终止、合流的规则集，

2. 失败终止，或

3. 无限循环。

请注意，用于构造 Gröbner 基的 Buchberger 算法与 Knuth-Bendix 完备化算法非常相似。