the Identity Problem for Semigroups

[AthlonAMDx64]

Hallo! How to solve the Identity Problem for Semigroups in Z3?
like "formulas(assumptions).(xy)z=x(yz).x1x2=(((x1x1)*x1)*x1)x2.((((((x1x2)*x1)*x2)*x1)*x2)*x1)x2=(((x1x2)*x2)*x2)x2.((x1x2)*x3)x4=(((((x1x2)*x1)*x1)*x1)*x3)x4.end_of_list.formulas(goals).((((c1c1)*c2)*c2)*c1)c2=((((c1c1)*c2)*c1)*c2)*c2.end_of_list." in Prover9

[NikolajBjorner]

z3 is not well-suited for proving theorems in universal algebra.
You would need to use quantifiers to encode your problem. Follow the online tutorial. https://microsoft.github.io/z3guide/

[AthlonAMDx64]

Are there any working examples of how to program the solution to the word equality problem in a semigroup using these quantifiers? I only learned about Z3Prover yesterday, so I don't even know where to start solving it or if it is even solvable using Z3.

[philzook58]

I have a hard time parsing what this prover9 problem is. This is my best guess as a z3 python script

from z3 import *

G = DeclareSort('G')
mul = Function("mul", G, G, G)
x1,x2,x3,x4 = Consts('x1 x2 x3 x4', G)
x,y,z = Consts('x y z', G)
s = Solver()
ExprRef.__mul__ = lambda x,y: mul(x,y)
s.add(ForAll([x,y,z], mul(x,mul(y,z)) == mul(mul(x,y),z)))
s.add(x1  * x2 == x1 * x1 * x1 *x1 * x2)
s.add(x1 * x2 * x1 * x2 * x1 * x2 * x1 * x2 == x1 * x2 * x2 * x2 * x2)
s.add(x1 * x2 * x3 * x4 == x1 * x2 *x1 *x1 *x1 *x3 * x4)

s.add(Not(x1 * x1 * x2 * x2 * x1 *x2 == x1 * x1 *x2 *x1 * x2 * x2))
s.check()

As mentioned, z3 is probably not the best tool for this job. If prover9 is working, go with that. GAP has special stuff in it for finitely presented semigroups https://docs.gap-system.org/doc/ref/chap51_mj.html#X8665D8737FDD5B10 https://www.gap-system.org/Packages/semigroups.html I'd suspect that would do best.

Out of curiousity, is there somewhere this problem is coming from?

[AthlonAMDx64]

Prover9 problem: if for any words x,y,z,t the identities (xy)z=x(yz), xy=(x^4)y, (xy)^4=x(y^4), xyzt=xy(x^3)zt hold;
then will the equality aabbab=aababb hold?
Prover9 do not have ancwer.
Personally, I have to check this when constructing a series of examples of semigroups with planar Cayley graphs. In general case the word equality problem is actively used in steganography algorithms.
PS: thank you very much for your quick answers!

[NikolajBjorner]

You should try https://tptp.org/cgi-bin/SystemOnTPTP with associated documents. There are several samples and newer theorem provers than Prover9.

[AthlonAMDx64]

Very good project. And you, as one of its founders, can you give me a link to an example of solving the problem "if for any words x,y,z,t the identities (xy)z=x(yz), xy=(x^4)y, (xy)^4=x(y^4), xyzt=xy(x^3)zt hold; then will the equality aabbab=aababb hold?" In https://tptp.org/cgi-bin/SeeTPTP?Category=Problems there are more logical problems than theorems from algebra