The Andrews-Curtis Conjecture, Term Rewriting and First-Order Proofs

  • A. LisitsaEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10931)


The Andrews-Curtis conjecture (ACC) 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 into a trivial presentation by a sequence of simple transformations. It is generally believed that the conjecture may be false and there are several series of potential counterexamples for which required simplifications are not known. Finding simplifications poses a challenge for any computational approach - the search space is unbounded and the lower bound on the length of simplification sequences is known to be at least superexponential. Various specialised search algorithms have been used to eliminate some of the potential counterexamples. In this paper we present an alternative approach based on automated reasoning. We formulate a 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. We report on the experiments demonstrating the efficiency of the proposed method by finding required simplifications for several new open cases.


  1. 1.
    Akbulut, S., Kirby, R.: A potential smooth counterexample in dimension 4 to the Poincare conjecture, the Schoenflies conjecture, and the Andrews-Curtis conjecture. Topology 24(4), 375–390 (1985)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Andrews, J., Curtis, M.L.: Free groups and handlebodies. Proc. Amer. Math. Soc. 16, 192–195 (1965)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)CrossRefGoogle Scholar
  4. 4.
    Baumslag, G., Myasnikov, A.G., Shpilrain, V.: Open Problems in Combinatorial Group Theory, 2nd edn., vol. 296, pp. 1–38. Amer. Math. Soc., Providence, RI (2002)Google Scholar
  5. 5.
    Birkhoff, G.: On the structure of abstract algebras. In: Mathematical Proceedings of the Cambridge Philosophical Society, vol. 31, pp. 433–454. Cambridge University Press (1935)CrossRefGoogle Scholar
  6. 6.
    Borovik, A.V., Lubotzky, A., Myasnikov, A.G.: The finitary Andrews-Curtis conjecture. In: Bartholdi, L., Ceccherini-Silberstein, T., Smirnova-Nagnibeda, T., Zuk, A. (eds.) Infinite Groups: Geometric, Combinatorial and Dynamical Aspects. Progress in Mathematics, vol. 248, pp. 15–30. Birkhäuser Basel (2005).
  7. 7.
    Bridson, M.R.: The complexity of balanced presentations and the Andrews-Curtis conjecture. ArXiv e-prints, April 2015Google Scholar
  8. 8.
    Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Formal Models and Semantics. Handbook of Theoretical Computer Science, vol. B, pp. 243–320. Elsevier, Amsterdam (1990)Google Scholar
  9. 9.
    Edjvet, M., Swan, J.: Irreducible cyclically presented groups 2005–2010.
  10. 10.
    Edjvet, M., Swan, J.: On irreducible cyclic presentations of the trivial group. Exp. Math. 23(2), 181–189 (2014)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Havas, G., Ramsay, C.: Andrews-Curtis and Todd-Coxeter proof words. Technical report, in Oxford, vol. I, London Math. Soc. Lecture Note Ser (2001)Google Scholar
  12. 12.
    Havas, G., Ramsay, C.: Breadth-first search and the Andrews-Curtis conjecture. Int. J. Algebra Comput. 13(01), 61–68 (2003)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Krawiec, K., Swan, J.: Ac-trivialization proofs eliminating some potential counterexamples to the Andrews-curtis conjecture (2015).
  14. 14.
    Lishak, B.: Balanced finite presentations of the trivial group. ArXiv e-prints, April 2015Google Scholar
  15. 15.
    Lisitsa, A.: First-order theorem proving in the exploration of Andrews-Curtis conjecture. TinyToCS 2 (2013)Google Scholar
  16. 16.
    McCaul, S.B., Bowman, R.S.: Fast searching for Andrews-Curtis trivializations. Exp. Math. 193–197, 2006 (2006)MathSciNetzbMATHGoogle Scholar
  17. 17.
    McCune, W.: Prover9 and mace4, 2005–2010.
  18. 18.
    Miasnikov, A.D.: Genetic algorithms and the Andrews-curtis conjecture. Int. J. Algebra Comput. 09(06), 671–686 (1999)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Plaisted, D.A.: Equational reasoning and term rewriting systems. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 1, pp. 274–364. Oxford University Press Inc, New York (1993)Google Scholar
  20. 20.
    Swan, J., Ochoa, G., Kendall, G., Edjvet, M.: Fitness landscapes and the Andrews-Curtis conjecture. IJAC 22(2) (2012)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Department of Computer ScienceUniversity of LiverpoolLiverpoolUK

Personalised recommendations