Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
https://zenodo.org/record/1248986 DOI: 10.5281/zenodo.1248986.
References
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)
Andrews, J., Curtis, M.L.: Free groups and handlebodies. Proc. Amer. Math. Soc. 16, 192–195 (1965)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)
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)
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)
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). https://doi.org/10.1007/3-7643-7447-0_2
Bridson, M.R.: The complexity of balanced presentations and the Andrews-Curtis conjecture. ArXiv e-prints, April 2015
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)
Edjvet, M., Swan, J.: Irreducible cyclically presented groups 2005–2010. https://www.maths.nottingham.ac.uk/personal/pmzme/Irreducible-Cyclically-Presented-Groups.pdf
Edjvet, M., Swan, J.: On irreducible cyclic presentations of the trivial group. Exp. Math. 23(2), 181–189 (2014)
Havas, G., Ramsay, C.: Andrews-Curtis and Todd-Coxeter proof words. Technical report, in Oxford, vol. I, London Math. Soc. Lecture Note Ser (2001)
Havas, G., Ramsay, C.: Breadth-first search and the Andrews-Curtis conjecture. Int. J. Algebra Comput. 13(01), 61–68 (2003)
Krawiec, K., Swan, J.: Ac-trivialization proofs eliminating some potential counterexamples to the Andrews-curtis conjecture (2015). www.cs.put.poznan.pl/kkrawiec/wiki/uploads/Site/ACsequences.pdf
Lishak, B.: Balanced finite presentations of the trivial group. ArXiv e-prints, April 2015
Lisitsa, A.: First-order theorem proving in the exploration of Andrews-Curtis conjecture. TinyToCS 2 (2013)
McCaul, S.B., Bowman, R.S.: Fast searching for Andrews-Curtis trivializations. Exp. Math. 193–197, 2006 (2006)
McCune, W.: Prover9 and mace4, 2005–2010. http://www.cs.unm.edu/~mccune/prover9/
Miasnikov, A.D.: Genetic algorithms and the Andrews-curtis conjecture. Int. J. Algebra Comput. 09(06), 671–686 (1999)
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)
Swan, J., Ochoa, G., Kendall, G., Edjvet, M.: Fitness landscapes and the Andrews-Curtis conjecture. IJAC 22(2) (2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Appendix
Appendix
5.1 Technical Details
We used Prover9 and Mace4 version 0.5 (December 2007) [17] and one of the two following system configurations:
-
(A)
AMD A6-3410MX APU 1.60 Ghz, RAM 4 GB, Windows 7 Enterprise
-
(B)
Intel(R) Core(TM) i7-4790 CPU 3.60 Ghz, RAM 32 GB, Windows 7 Enterprise
“t/o” stands for timeout in 200s; “GC” means encoding with ground conjugation rules; all other encodings are with non-ground conjugation rules.
5.2 AC-Trivialization for T16
Initial presentation:
\(\langle a,b,c \mid ABCacbb,BCAbacc, CABcbaa\rangle \)
Simplification:
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Lisitsa, A. (2018). The Andrews-Curtis Conjecture, Term Rewriting and First-Order Proofs. In: Davenport, J., Kauers, M., Labahn, G., Urban, J. (eds) Mathematical Software – ICMS 2018. ICMS 2018. Lecture Notes in Computer Science(), vol 10931. Springer, Cham. https://doi.org/10.1007/978-3-319-96418-8_41
Download citation
DOI: https://doi.org/10.1007/978-3-319-96418-8_41
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-96417-1
Online ISBN: 978-3-319-96418-8
eBook Packages: Computer ScienceComputer Science (R0)