Using ϵ -unification and Knuth-Bendix completion to automatically proof theorems about groups
This is going to be a somewhat incomplete answer, since you are asking some pretty broad questions about the applications of the techniques.

First let me start by saying that while the research in the field of equational logic and completion hasn't seen a complete revolution since 1980 (as compared to, say SMT) there have been substantial improvements, so bear in mind that techniques and tools have changed. My first recommendation would be to take a look at Term Rewriting and All That by Baader and Nipkow, which is slightly more up to date (but still almost 20 years old!). You might also want to check CiME as an implementation of some of these techniques.

The canonical set from the first example of the appendix is actually

$\begin{eqnarray}R1 &amp;:&amp; 0+X\rightarrow X\\R2&amp;:&amp;I(X)+X\rightarrow 0\\R3&amp;:&amp;(X+Y)+Z\rightarrow X+(Y+Z)\\R8&amp;:&amp;I(0)\rightarrow 0\\R11&amp;:&amp;X+0\rightarrow X\\R12&amp;:&amp;I(I(X))\rightarrow X\\R13&amp;:&amp;X+I(X)\rightarrow 0\\R14&amp;:&amp;X+(I(X)+Y)\rightarrow Y\\R17&amp;:&amp;I(X+Y)\rightarrow I(Y)+I(X)\end{eqnarray}$

For the life of me I can't understand why they adopted additive notation for non-commutative groups.

Note that the set $\{R1,R2,R3\}$ is not canonical, since e.g. $X+0$ does not reduce to $0$ (but $X+0=0$ is derivable in the equationnal system).

The canonical system was derived from the first 3 rules by application of Kuth-Bendix completion, and nothing else, $\varepsilon$-unification is not needed in this case. There are many papers that expand on this example, including, I think, the original paper which is sadly tough to find online. The wikipedia page is a good place to fish for references.

I'm not sure what advice to recommend for using these techniques in practice. I gave a reference to an existing tool, there are many others in various states of maintenance, see e.g. here.

I would also suggest taking a look at first-order theorem provers with equality and equality logic provers, e.g. Otter &amp; Mace since they integrate these kinds of techniques and might be more suited to your needs, if you're trying to prove basic theorems in some algebraic theory.

I really suspect you might want some more specialized tools for Gröbner bases if you're trying to prove theorems about fields, since these are much more specialized (and much more powerful). Perhaps some people more familiar with computer algebra can point you in the right direction for this.