Stable Andrews-Curtis trivialization of AK(3) revisited. A case study using automated deduction
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912211561086976 |
|---|---|
| author | Lisitsa, Alexei |
| author_facet | Lisitsa, Alexei |
| contents | Recent work by Shehper et al. (2024) demonstrated that the well-known Akbulut-Kirby AK(3) balanced presentation of the trivial group is stably AC-equivalent to the trivial presentation. This result eliminates AK(3) as a potential counterexample to the stable Andrews-Curtis conjecture. In this paper, we present an alternative proof of this result using an automated deduction approach. We provide several transformation sequences, derived from two different proofs generated by the automated theorem prover Prover9, that certify the stable AC-equivalence of AK(3) and the trivial presentation. We conclude by proposing a challenge to develop computational methods for searching stable AC-transformations. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_18601 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Stable Andrews-Curtis trivialization of AK(3) revisited. A case study using automated deduction Lisitsa, Alexei Logic in Computer Science Group Theory 20-08 Computational methods for problems pertaining to group theory I.2.3 Recent work by Shehper et al. (2024) demonstrated that the well-known Akbulut-Kirby AK(3) balanced presentation of the trivial group is stably AC-equivalent to the trivial presentation. This result eliminates AK(3) as a potential counterexample to the stable Andrews-Curtis conjecture. In this paper, we present an alternative proof of this result using an automated deduction approach. We provide several transformation sequences, derived from two different proofs generated by the automated theorem prover Prover9, that certify the stable AC-equivalence of AK(3) and the trivial presentation. We conclude by proposing a challenge to develop computational methods for searching stable AC-transformations. |
| title | Stable Andrews-Curtis trivialization of AK(3) revisited. A case study using automated deduction |
| topic | Logic in Computer Science Group Theory 20-08 Computational methods for problems pertaining to group theory I.2.3 |
| url | https://arxiv.org/abs/2501.18601 |