Some experiments with a completion theorem prover (Q1186705)

This paper is intended to show how an automatic theorem prover, which uses the completion algorithm, can solve problems in algebra. The results have been obtained using version 2.4 of the prover REVE (one of the most important author is Pierre Lescanne). The completion algorithm takes as input a set of equations and rules and an ordering, and constructs new rules by ordering equations, and new equations by computing critical pairs. A complete (terminating and confluent) set of rules equivalent to a given set of equations gives a solution to the word problem in the variety which is defined by the equations. Of course, since not all algebraic systems have a decidable word problem, there are systems for which no finite complete set of rules can be found. The authors show how REVE solves a series of standard ``test problems'': homomorphisms and automorphisms of groups, alternative axiomatization of groups, ternary algebra, non-associative rings, the Fibonacci groups. There are 18 examples, each of them with the input equations and with a complete set of rewrite rules output. Some cases, where the completion algorithm diverges, are presented, especially when the operator precedence is changed.