Single axioms for groups and abelian groups with various operations (Q1312155)

The author gives a survey of single law definitions for the variety of groups and for the variety of abelian groups in terms of various combinations of binary, unary, and nullary operations, where the binary operation is multiplication or right division or double division [that is, multiplication of inverses], the unary operation is inversion, and the nullary operation produces the neutral element of multiplication [alias the unit element]. There are six combinations that yield such single laws, both for groups and for abelian groups, so 12 laws are exhibited. The ``type'' of a law \(u=v\), where \(v\) is a single variable, is \(\langle L,N,D\rangle\), where \(L\) is the length of \(u\) [that is the number of occurrences of variables and operators], \(N\) is the number of variable occurrences in \(u\), and \(D\) is the number of distinct variables in the law. A number of such laws have been found before [see the paper by \textit{K. Kunen} reviewed above (Zbl 0794.20001) and the literature quoted in that review: there are many more papers in existence, of varying relevance to the author's aim]. The author's laws are new, and in all but two of the cases where laws were previously known, they are also shorter [the two laws where no shorter laws were found are the ones in terms of right division of \textit{G. Higman} and \textit{B. H. Neumann} in the paper quoted in the preceding review, which are of type \(\langle 17,9,3\rangle\) and \(\langle 9,5,3\rangle\), respectively]. The author also presents a counterexample to the reviewer's Theorem 2 [in Ill. J. Math. 30, 295-300 (1986; Zbl 0581.20004)=Selected works of \textit{B. H. Neumann} and \textit{Hanna Neumann}, Winnipeg, Canada (1988; Zbl 0655.20001), Vol. V, 1098-1103]. The method of the author relies on the automated theorem proving program OTTER, as well as on some other programs, such as FINDER. Simplified versions of the proofs of two of the laws, as found by OTTER, are presented. As one would expect, the associative law in the last of the group laws [or abelian group laws] to be proved. \{The notation is traditional, so that parentheses have to be extensively used\}.