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?