Automated reasoning boosted by a probabilistic automaton classifier: An application to the Andrews-Curtis conjecture

Abstract Automated reasoning can take a prohibitively long time to run. We present a combined approach which makes automated reasoning more efficient by using supervised learning to identify promising tasks for automated reasoning. For supervised learning, we have developed a new, simple and efficient way of training an automaton classifier. We demonstrate the efficiency of our approach on examples drawn from the Andrews-Curtis conjecture, a famously challenging problem.