Problem corner: Proving equivalence of different axiomatizations of free groups (Q1108815)

The authors have developed an automatic theorem prover based on lexicographic recursive path ordering [the authors, RRL: A rewrite rule laboratory - user's manual, GE R \& D Center (1987)] that transforms given formulas into normal forms and then uses substitution rules to derive new formulas. The authors use the program to show the equivalence of four axiomatizations of the notion of free group and to derive complete sets of rewrite rules for these constructs.