Automated reasoning in the exploration of Andrews-Curtis conjecture

Automated reasoning in the exploration of Andrews-Curtis Conjecture

Proving or disproving the Andrews-Curtis conjecture [1] remains one of the outstanding open problems in combinatorial group theory. In short, it states that every balanced presentation of the trivial group can be transformed (aka. AC-simplified) into a trivial presentation by a sequence of Nielsen transformations on the relators together with conjugations of relators.
It is believed that the conjecture may well be false and there are several potential (series of) counterexamples for which required simplifications are not known. Specialized search algorithms, including genetic search algorithms have been used so far to refute the potential counterexamples, see recent overview in [3].
We propose an alternative approach [4,5] and formulate the term rewriting system ACT for AC-transformations, and its translation(s) into the first-order logic. The problem of finding AC-simplifications is reduced to the problem of proving first-order formulae, which is then tackled by the available automated theorem provers.
Our experiments using automated Prover9 show that for all proposed potential counterexamples where non-trivial AC-simplifications were found by specialised search algorithms, AC-simplifications can be found by the generic theorem proving too. That opens an opportunity to apply present and future developments in automated theorem proving to the exploration of Andrews-Curtis conjecture.

In [5] we demontsrate novel AC-simplifications obtained by automated theorem proving.

Case Study

To demonstrate our apporach consider well-known presentation [a,b|aab'b'b',abab'a'b'] of trivial group which had been potential counterexample to AC-conjecture until [2] where it was shown using genetic search algorithms that this presentation is in fact AC-equivalent to trivial presentation.
Now we formulate the term rewriting system ACT_2 for AC-transformations for the presentations with two relators.
The vocabulary consists of binary functional symbol * which we use in infix notation, unary symbol ' which we use in posfix notaion, constant symbol e and binary functional symbol f.
Rewriting rules of ACT_2 are

f(x,y) -> f(x',y)
f(x,y) -> f(x,y')
f(x,y) -> f(x,y*x)
f(x,y) -> f(x*y,x)
f(x,y) -> f((z*x)*z',y)
f(x,y) -> f((z'*x)*z,y)

Now we consider rewriting by ACT_2 modulo equational theory of groups G:

e*x = x
x *e = x
x' * x = e
x * x' = e
(x * y) * z = x * (y *z)

(Notice this is not minimal formulation of equational theory of groups; using any other here won't affect anything in our approach).

Now the statement "the presentation [a,b|aab'b'b',abab'a'b'] does satisfy the conditions of AC-conjecture" is equivalent to the statement "the term f(a*a*b'*b'*b',a*b*a*b'*a*b') can be rewritten by ACT_2 modulo G to the term f(a,b)". We notice further that the transitive closure of ACT_2 modulo G rewriting relation is symmetric. Because of that we can equivalently reformulate the last statement in terms of the equational theory ACT_2_G, consisting the following equalities:

f(x,y) = f(x',y)
f(x,y) = f(x,y')
f(x,y) = f(x,y*x)
f(x,y) = f(x*y,x)
f(x,y) = f((z*x)*z',y)
f(x,y) = f((z'*x)*z,y)
e*x = x
x *e = x
x' * x = e
x * x' = e
(x * y) * z = x * (y *z)

(i.e all rewriting rules of ACT_2 replaced by equalities and joined with G).
Now we have an equivalent reformualtion of the last statement in terms of ACT_2_G, that is "ACT_2_G implies f(a*a*b'*b'*b',a*b*a*b'*a*b') = f(a,b)".
At this point we delegate the task of proving the last condition to the automated theorem prover Prover9. It took 25.60 seconds for Prover9 running on a laptop of average specification to prove the statement refuting thereby above presentation as a counterexample to AC-conjecture. Here is the proof.

References

[1] Andrews, J. J.; Curtis, M. L. (1965), "Free groups and handlebodies", Proceedings of the American Mathematical Society (American Mathematical Society) 16 (2): 192–195
[2] Alexei D. Miasnikov, Genetic algorithms and the Andrews-Curtis conjecture, International Journal of Algebra and Computation, 9(6):671-686,1999
[3] J. Swan, G. Ochoa, G. Kendall, M. Edjvet (2012) Fitness Landscapes and the Andrews-Curtis Conjecture, International Journal of Algebra and Computation, Vol. 2, No. 22, pp. 125009 (13 pages)
[4] Alexei Lisitsa: First-order theorem proving in the exploration of Andrews-Curtis conjecture. TinyToCS 2 (2013)
[5] Alexei Lisitsa: The Andrews-Curtis Conjecture, Term Rewriting and First-Order Proofs, in James Davenport et al. eds, Mathematical Software -- ICMS 2018, LNCS 10931, 2018, 343--351