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

Lisitsa, A (2018) The Andrews-Curtis Conjecture, Term Rewriting and First-Order Proofs. In: ICMS 2018.

Text The_Andrews_Curtis_conjecture__term_rewriting_and_first_order_proofs.pdf - Author Accepted Manuscript Download (355kB)

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.

Item Type:	Conference or Workshop Item (Unspecified)
Depositing User:	Symplectic Admin
Date Deposited:	15 Jan 2019 14:56
Last Modified:	19 Jan 2023 01:25
DOI:	10.1007/978-3-319-96418-8_41
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3025904