O'Reilly logo

Handbook of Automated Reasoning by Andrei Voronkov, Alan J.A. Robinson

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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.  S

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required