This is a follow-up question. In my previous question, I presented Welder proof assistant and I stated that I want to automate proofs about basic field theory. The only answer to this post states that a combinatorial search is sufficient since the goals are easy. I'm looking for a more general technique. I have read Equations and rewrite rules: a survey. In page 12, it reads:An abelian group theory unification algorithm is given by Lankford.The idea is as follows. Given some context equations $\Delta$ from where we can deduce some other equations $\Delta \vDash \{x_i = y_i\}$, the unification process will give the neccesary substitutions to proof all the equalities in the right part using the formulas in $\Delta$. Another interesting quote appears on page 28:This algorithm gave the first known solution to unification in group  theory using for $\mathcal{B}$ the canonical set shown in the  appendix.In the appendix on page 33, I find a very interesting practical session. I have some questions on the power of the methods used and the actual results that I can expect after well-understanding this 30 pages heavy mathematical paper. I hope someone can give some orientation:What is being simulated in the practical session? I describe what I think is happening. The canonical set $\mathcal{B}$ mentioned above corresponds to given axioms $R_1$, $R_2$ and $R_3$. Then some theorems about groups are deduced. I assume that this happens by application of the $\epsilon$-unification algorithm given at page 27 and the Knuth-Bendix completion. Am I right? Could you tell me what is exactly the role of each algorithm (page 27 and Knuth-Bendix) in the solution? If you think that I can use this scheme in my problem, what steps should I do, how should I integrate this algorithms?
Using  -unification and Knuth-Bendix completion to automatically proof theorems about groups
lo.logic;proof assistants;term rewriting systems