Estoy buscando algunos matemáticos software que me pueda ayudar con una tarea muy habitual en el ámbito de álgebra universal (que yo sepa programas como prover9/mace4 y uacalc no ayuda con este problema).
La entrada de este software debe ser de dos diferentes finito álgebra de operadores, cada uno de ellos, dado a través de la mesa de sus operaciones. Por lo tanto, los casos particulares están considerando dos grupos finitos, dos álgebras Booleanas, etc.
La respuesta (en caso de que el equipo de búsqueda se encuentra algo) de este software debe ser una ecuación que puede distinguir a estos dos finito álgebras en el sentido de que es válido en uno de ellos, mientras no válida en el otro álgebra. La idea es que el software busca automáticamente una ecuación en la correspondiente expresión algebraica de la firma de tal manera que es válido en una de estas álgebras pero no es válido en el otro. Por ejemplo, si consideramos las dos finito álgebras de ser el aditivo grupos de $\mathbb{Z}/2$ $\mathbb{Z}/3$ una ecuación que es válida en $\mathbb{Z}/2$, pero no en $\mathbb{Z}/3$$x + x = y + y$; por lo tanto $x+x = y+y$ es un ejemplo del tipo de respuesta que estoy buscando. Por otro lado, no hay una ecuación para distinguir la $2$ elementos del álgebra Booleana a partir de la $4$ elementos de tipo Booleano; por lo tanto, en este caso, el equipo de búsqueda se ejecutará siempre, sin ofrecer una respuesta.
En caso de que alguien sabe de un software para hacer la tarea anterior, permítanme señalar que también estoy interesado en obtener respuestas de delimitación del número de variables que aparecen en las ecuaciones. Aquí me refiero a obtener respuestas de los siguientes tipos: con las ecuaciones que sólo el uso de $3$ variables que no hay manera de distinguir estos dos finito álgebras, con las ecuaciones que sólo el uso de $4$ variables que no hay manera de distinguir estos dos finito álgebras, y con las ecuaciones que sólo el uso de $5$ variables podemos distinguir el uso de este explícita de la ecuación (la dada por el software como respuesta).
