Knuth-Bendix procedure and non deterministic behavior. An example
Résumé
In this note, we present and study a typical example to illustrate the non determinism of the Knuth-Bendix algorithm with respect to the ordering it uses. Our example shows how different orderings on terms lead to different completion processes, and how eleven different completion sessions produce only two different rewrite systems.