Single axioms for groups
This paper demonstrates the difference of approach to proving certain mathematical facts by an oldfashioned mathematician [like the reviewer] and a mathematician versed in theorem proving by computers, and it illustrates the strength of the latter approach. The reviewer had found various single axioms that define the variety of groups in terms of a binary operation, namely multiplication or multiplication of inverses, and a unary operation, namely inversion [\textit{B. H. Neumann}, Bull. Aust. Math. Soc. 23, 81-102 (1981; Zbl 0581.20003), 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, 1076- 1097, 1098-1103]. The laws were of the form \(u=v\), where \(v\) had length 1 and \(u\) had length 18 and involved 4 variables; and the reviewer conjectured that these numbers could not be reduced. The author disproves these conjectures by exhibiting laws with \(u\) of length 18 in only 3 variables and with \(u\) of length 16 in 4 variables. These laws were found by the author and by \textit{W. W. McCune} [see the following review Zbl 0794.20002] using the automated theorem-proving program OTTER. The author first proves explicitly some known results, which were stated, without proof [``not very difficult to prove \dots We omit the proofs] by \textit{G. Higman} and \textit{B. H. Neumann} [Publ. Math. 2, 215-221 (1953; Zbl 0050.25303) = Selected works of \textit{B. H. Neumann} and \textit{Hanna Neumann}, Winnipeg, Canada (1988; Zbl 0655.20001), Vol. V, 1069-1075]. For example, to prove the known result that at least 3 variables are needed in the laws, the author exhibits an elegant Moufang loop of order 10, which is, moreover, boolean: this, apparently the smallest properly non-associative di-associative loop, was also found using a computer program. The computer was also extensively used to prove other results contained in the literature, for example that at least three inversions must occur. The author exhibits 8 laws of the above form, in 3 variables, with \(u\) in 4 of them of length 18 and in 4 of length 20; some obvious transformations quadruple the laws to 32. The difference in lengths stems from the fact that the first 4 laws contain 5 inversions in \(u\), the last 4 contains 7. The author conjectures that fewer than 5 inversions will not suffice, and states some more unsolved problems. \{The reviewer found the notation difficult to follow, because it is traditional functional notation, which requires numerous separators, namely commas and parentheses\}.
- Single axioms for groups and abelian groups with various operations
- The shortest single axioms for groups of exponent 4
- On single-law definitions of groups
- Another single law for groups
- Yet another single law for groups
- Computer and Human Reasoning: Single Implicative Axioms for Groups and for Abelian Groups
- scientific article; zbMATH DE number 1324436
- Searching for shortest single axioms for groups of exponent \(6\)
- Solution of the Robbins problem
- scientific article; zbMATH DE number 3922990
- Yet another single law for groups
- Group axioms for iteration
- Single axioms for groups and abelian groups with various operations
- The shortest single axioms for groups of exponent 4
- Single axioms for odd exponent groups
- OTTER experiments in a system of combinatory logic
- Basis reduction for cryptogroups and orthogroups
- Single axioms: With and without computers
- Shortest single axioms with neutral element for groups of exponent 2 and 3.
- Computer solutions of problems in inverse semigroups.
- scientific article; zbMATH DE number 3912595 (Why is no real title available?)
- Another single law for groups
- scientific article; zbMATH DE number 120344 (Why is no real title available?)
- scientific article; zbMATH DE number 2064560 (Why is no real title available?)
- A method for finding new sets of axioms for classes of semigroups.
- System description generating models by SEM
- A lower bound of the number of rewrite rules obtained by homological methods
- A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods
- Fiala-Agre list of single axioms for Boolean groups is wrong
- A shortest single axiom with neutral element for commutative Moufang loops of exponent 3
- Absolutely Independent Group Axioms
- Ken Kunen: algebraist.
- Automated discovery of new axiomatizations of the left group and right group calculi
- Anick resolutions for lawvere theories via algebraic discrete Morse theory
- Searching for shortest single axioms for groups of exponent \(6\)
- Applying SAT solving in classification of finite algebras
- Automatic construction and verification of isotopy invariants
This page was built for publication: Single axioms for groups
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q688567)
