kdrag.solvers.kb.basic

kdrag.solvers.kb.basic(E, order=<function kbo>)

Basic Knuth Bendix completion algorithm.

TRaaT 7.1.1 Central Groupoid example

>>> import kdrag as kd
>>> T = smt.DeclareSort("CentralGroupoid")
>>> x,y,z = smt.Consts("x y z", T)
>>> mul = smt.Function("mul", T, T, T)
>>> kd.notation.mul.register(T, mul)
>>> E = [smt.ForAll([x,y,z], (x * y) * (y * z) == y)]
>>> assert len(basic(E)) == 3