With the aid of automated reasoning techniques, we show that all previously known short single axioms for odd exponent groups are special cases of one general schema. We also demonstrate how to convert the proofs generated by an automated reasoning system into proofs understandable by a human.
This is a preview of subscription content, log in to check access.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
Beth, T., Jungnickel, D., and Lenz, H.:Design Theory, Bibliographisches Institut, 1985.
Kunen, K.: Single axioms for groups,J. Automated Reasoning 9 (1992), 291–308.
Kunen, K.: The shortest single axioms for groups of exponent 4, Technical Report UW#1134, University of Wisconsin, 1993;Computers and Mathematics with Applications 29 (1995), 1–12.
McCune, W. W.: OTTER 3.0 reference manual and guide, Technical Report ANL-94/6, Argonne National Laboratory, 1994.
McCune, W. W.: Single axioms for groups and Abelian groups with various operations,J. Automated Reasoning 10 (1993), 1–13.
McCune, W. W. and Wos. L.: Applications of automated deduction to the search for single axioms for exponent groups, inLogic Programming and Automated Reasoning, Springer-Verlag, 1992, pp. 131–136.
Neumann, B. H.: Another single law for groups,Bull. Australian Math. Soc. 23 (1981), 81–102.
Tarski, A.: Equational logic and equational theories of algebras, in H. A. Schmidt, K. Schütte, and H.-J. Thiele (eds),Proc. Logic Colloquium, Hannover, 1966, North-Holland, 1968, pp. 275–288.
Authors supported by NSF Grant DMS-9100665
About this article
Cite this article
Hart, J., Kunen, K. Single axioms for odd exponent groups. J Autom Reasoning 14, 383–412 (1995). https://doi.org/10.1007/BF00881714
- single axioms
- odd exponent group
AMS subject classification