# Software for some universal algebra issues

I am looking for some mathematical software that can help me with a very common task in the realm of universal algebra (as far as I know programs like prover9/mace4 and uacalc do not help with this issue).

The input of this software should be two different finite algebras, each of them given through the table of its operations. Thus, particular cases are considering two finite groups, two Boolean algebras, etc.

The answer (in case the computer search finds something) of this software should be an equation that can distinguish these two finite algebras in the sense that it is valid in one of them, while not valid in the other algebra. The idea is that the software automatically searches for an equation in the corresponding algebraic signature such that it is valid in one of these algebras but not valid in the other one. For instance, if we consider the two finite algebras to be the additive groups of $\mathbb{Z}/2$ and $\mathbb{Z}/3$ an equation that is valid in $\mathbb{Z}/2$ but not in $\mathbb{Z}/3$ is $x + x = y + y$; hence $x+x = y+y$ is an example of the kind of answer I am looking for. On the other hand, there is not such an equation to distinguish the $2$ elements Boolean algebra from the $4$ elements Boolean one; hence, in this case, the computer search will run forever without providing an answer.

In case anyone knows a software to do the previous task, let me point out that I am also interested in getting answers bounding the number of variables appearing in the equations. Here I refer to getting answers of the following kind: with equations that only use $3$ variables there is no way distinguish these two finite algebras, with equations that only use $4$ variables there is no way distinguish these two finite algebras, and with equations that only use $5$ variables we can distinguish them using this explicit equation (the one given by the software as answer).

-
The Universal Algebra Calculator can do many wonderful things, and it can probably do what you want. For example, given algebras A and B, of the same type, I believe it can determine whether Clo(B) $\subseteq$ Clo(A), and if they are not equal it will produce a term operation that is in the latter but not in the former. However, some of these features are very new, and not yet documented. – William DeMeo Feb 22 '12 at 4:21
Correction to my comment above: You don't want to assume A and B have the same type! (but you do want to assume they are on the same set) Also, my comment doesn't answer your question, but the post below, by Ralph Freese (user25460), does. – William DeMeo Feb 23 '12 at 2:51