Knuth–Bendix completion

Definition

Let $T$ be the set of terms over a signature and a set of variables. Let $E$ be a finite set of equations $s \approx t$ between terms. Let $>$ be a reduction order on $T$, that is, a strict order with these properties. It is well-founded, and $s > t$ implies $C[s] > C[t]$ for every context $C$ and $\sigma(s) > \sigma(t)$ for every substitution $\sigma$. Let $l_1 \to r_1$ and $l_2 \to r_2$ be rules with disjoint variables. Let $p$ be a position of $l_1$ where the subterm $l_1|_p$ is not a variable and has a most general unifier $\sigma$ with $l_2$. Then the pair $(\sigma(r_1), \sigma(l_1)[\sigma(r_2)]_p)$ is a critical pair. The Knuth–Bendix completion procedure, with input $E$ and $>$, maintains a set $R$ of rules of a term rewriting system:

1. To orient an equation $s \approx t$ with $s \ne t$: add $s \to t$ to $R$ if $s > t$, add $t \to s$ if $t > s$, and stop with failure otherwise.
2. Start with $R = \emptyset$ and orient every equation of $E$.
3. For each critical pair $(s, t)$ of rules of $R$, compute normal forms $s'$ of $s$ and $t'$ of $t$ with respect to $R$. If $s' \ne t'$, orient $s' \approx t'$.
4. Repeat step 3 until every critical pair of $R$ has equal normal forms, and then stop with output $R$.