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.

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)

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)

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.

[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