Thank you for sharing this!

One powerful tool that often helps when reasoning over algebraic structures is called Term Rewriting.

For example, let us consider the 6 equations from the paper that characterize loops, using Prolog syntax:

    loop([X*e = X,
          e*X = X,
          X\(X*Y) = Y,
          X*(X\Y) = Y,
          (Y*X)/X = Y,
          (Y/X)*X = Y]).

To closely adhere to the notation of the paper, I am using the following operator definition to use \ as an infix operator in the terms above:

    :- op(400, yfx, \).

Then, using a suitable implementation of a completion algorithm such as the Knuth-Bendix completion, we can - if we are lucky - actually turn these equations into a set of oriented rewrite rules:

    ?- loop(Ls),
       equations_trs(Ls, TRS),
       maplist(portray_clause, TRS).

In this case, I obtain the following term rewriting system (TRS) for the equations above:

    A/(B\A)==>B.
    A/A==>e.
    B*A/A==>B.
    A/B\A==>B.
    A/e==>A.
    B/A*A==>B.
    A\A==>e.
    A*(A\B)==>B.
    A*e==>A.
    e*A==>A.
    e\A==>A.
    A\(A*B)==>B.

As I said, these rules are oriented, and moreover they are also terminating, in contrast to the original equations which can be applied in any direction and (hence) arbitrarily often. Thus, deciding the equivalence of two terms subject to the above identities has been reduced to exhaustively applying these rewrite rules to both terms, and then checking whether they are reduced to the same normal form!

I always beg for links to abstracts rather than PDFs, but this one doesn't seem to be on the arXiv, so that's not so easy. Here's the one-level-up page: http://www.karlin.mff.cuni.cz/~stanovsk/qptp ; and the article page for the journal in which it appeared (AI Comm. 23 (2010) 2–3): http://content.iospress.com/articles/ai-communications/aic46... .

For more recent result of automated theorem proving in loop theory, see "Loops with abelian inner mapping groups: An application of automated deduction (2015)". https://arxiv.org/abs/1509.05468