Complete sets of reductions with constraints

Abstract

We show that by constraining the substitutions allowed in some of the rules, it is possible to find complete sets of reductions for equational theories which include non-orientable equations such as commutativity without requiring a special unification algorithm. We develop the theory for such constrained reductions and we exhibit complete sets for semilattices, boolean algebras, and ternary boolean algebras.