Using ϵ -unification and Knuth-Bendix completion to automatically proof theorems about groups

Question

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?

Answer 1

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 &:& 0+X\rightarrow X\\R2&:&I(X)+X\rightarrow 0\\R3&:&(X+Y)+Z\rightarrow X+(Y+Z)\\R8&:&I(0)\rightarrow 0\\R11&:&X+0\rightarrow X\\R12&:&I(I(X))\rightarrow X\\R13&:&X+I(X)\rightarrow 0\\R14&:&X+(I(X)+Y)\rightarrow Y\\R17&:&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 & 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.