Revision history [back]

You can compute a rewriting system by: rewrite = H3.rewriting_system()

Then rewrite.reduce(a1*b1/a1/b1*a2*b2/a2/b2*a3*b3/a3/b3) gives you 1 as expected. But the rewriting system is not confluent by default, and it only has the one rule: a1*b1*a1^-1*b1^-1*a2*b2*a2^-1*b2^-1*a3*b3*a3^-1*b3^-1 ---> 1.

In general, it is not possible to guarantee that the Knuth-Bendix procedure will terminate to produce a confluent rewriting system. This is why the system cannot automatically reduce arbitrary expressions. In fact, it seems that Knuth-Bendix fails to terminate on your example. See the make_confluent() documentation for more information.