Paper Info
Title
The Andrews-Curtis Conjecture, Term Rewriting and First-Order Proofs.
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.
Year
DOI
Venue
2018
10.1007/978-3-319-96418-8_41
Lecture Notes in Computer Science
Field
DocType
Volume
Automated reasoning,Discrete mathematics,Algebra,Computer science,Combinatorial group theory,Trivial group,Mathematical proof,Rewriting,Counterexample,Conjecture,Andrews–Curtis conjecture
Conference
10931
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
6
1
Name
Order
Citations
PageRank
Alexei Lisitsa127245.94