Single axioms for groups and abelian groups with various operations
type: Item
instance of: scholarly article
title: Single axioms for groups and abelian groups with various operations
zbMATH Open document ID: 0794.20002
DOI: 10.1007/BF00881862
author: William McCune
published in: Journal of Automated Reasoning
publication date: 1994-08-25T00:00:00Z
review text: 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 associa…
Mathematics Subject Classification ID: 20A05
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 20-04
zbMATH DE Number: 488231
zbMATH Keywords: type of a law
zbMATH Keywords: single law definitions
zbMATH Keywords: variety of groups
zbMATH Keywords: variety of abelian groups
zbMATH Keywords: nullary operations
zbMATH Keywords: binary operation
zbMATH Keywords: unary operation
zbMATH Keywords: inversion
zbMATH Keywords: length
zbMATH Keywords: automated theorem proving program OTTER
zbMATH Keywords: FINDER
Wikidata QID: Q114694138
reviewed by: B. H. Neumann
describes a project that uses: OTTER
describes a project that uses: FINDER
MaRDI profile type: Publication
cites work: Q5818498
cites work: Q3028369
cites work: Problem corner: Proving equivalence of different axiomatizations of free groups
cites work: Q5581665
cites work: Single axioms for groups
cites work: Automated discovery of new axiomatizations of the left group and right group calculi
cites work: Another single law for groups
cites work: Yet another single law for groups
cites work: Ein Beitrag zur Axiomatik der Abelschen Gruppen
cites work: Q5609363
full work available at URL: https://doi.org/10.1007/bf00881862
OpenAlex ID: W2044767417
Recommended article: On single-law definitions of groups
Recommended article: Single axioms for groups
Recommended article: The shortest single axioms for groups of exponent 4
Recommended article: Another single law for groups
Recommended article: Q4845127
Recommended article: Q3735931
Recommended article: Yet another single law for groups
Recommended article: Computer and Human Reasoning: Single Implicative Axioms for Groups and for Abelian Groups
Recommended article: Q4458213
Recommended article: Searching for shortest single axioms for groups of exponent \(6\)
description: scientific article; zbMATH DE number 488231