Handbook of Automated Reasoning

5.2 The class of commutative/monoidal theories

In order to generalize this semantic approach to a whole class of theories, let us try to determine the relevant common features of the theories ACU, ACUI, and AG. Using a rather syntactic point of view, we may observe that all three theories are concerned with an associative-commutative binary function symbol f with a unit e. In addition, the signature of AG contains a unary function symbol i, which behaves like an endomorphism for f and e, i.e., i(f(x,y)) = _AG f(i(x),i(y)) and i(e) = _AG e. This observation motivates the following definition of monoidal theories [Nutt 1990]:

5.1

Definition.

An equational theory E is called monoidal iff it satisfies the following properties:

1.  $\mathcal{S}$