A decidable equational theory with undecidable membership problem for finite algebras (Q1966168)

It was proved recently by R. Hirsch and I. Hodkinson that the variety of representable relation algebras has undecidable membership problem for finite algebras, i.e., there is no algorithm deciding whether a finite algebra belongs to the variety. Since the equational theory of representable relation algebras is undecidable, it is natural to ask if there is a variety with decidable equational theory but undecidable membership problem. The author gives an example of such a variety whose signature contains just two unary and two nullary operations.