Knuth-Bendix 完備化演算法

Knuth-Bendix 完備化演算法嘗試將有限的 恆等式 集合轉換為一個 有限終止、合流 的 項重寫系統，其歸約保持恆等性。這個項重寫系統充當驗證恆等式的判定程式。

正如在 泛代數 中定義的，恆等式是兩個 項 的等式: 。據推測，對於其中出現的所有變數的值，這兩個項的值都相等。 歸約序 是完備化演算法的另一個輸入，前提是將每個恆等式視為將左側轉換為右側，反之亦然的重寫規則的兩個候選者。

輸出的 項重寫系統 用於確定 是否是恆等式，方法如下。如果兩個不同的項 和 具有相同的正規化，則 是恆等式。否則， 不是恆等式。既是 有限終止 又是 合流 的項重寫系統享有對所有表示式都具有唯一正規化的性質。 決定 是否是恆等式的問題也稱為詞問題。

最初，該演算法嘗試根據歸約序定向輸入恆等式 (如果 ，則 成為規則)。 然後，它用匯出的規則完成這組初始規則。 該演算法迭代地檢測 臨界對，獲得它們的正規化，並根據 歸約序 為每對正規化新增新規則。

該演算法可能

1. 成功終止併產生一個有限終止、合流的規則集，

2. 失敗終止，或

3. 無限迴圈。

請注意，用於構造 Gröbner 基的 Buchberger 演算法與 Knuth-Bendix 完備化演算法非常相似。