²Sections 13.4 and 14.9 provide a command for computing minimal sets of, respectively, unifiers modulo axioms or modulo a convergent equational theory. Narrowing with rules modulo an equational theory has been extended to use a minimal set of unifiers.