String rewriting

This webpage allows you to compute the Knuth-Bendix completion of a string rewriting system (according to the deglex order). It is based on ocaml-alg, a generic library for manipulating algebraic data structures. A previous version (with more features but not maintained anymore) was called rewr.

Presentation

Classical: with n =

Generators:

Rules:

Order:

Results

Parsed presentation

Knuth-Bendix completion

Reduced completion

Coherence cells