Remote Access Mathematics of Computation
Green Open Access

Mathematics of Computation

ISSN 1088-6842(online) ISSN 0025-5718(print)



Semigroups, antiautomorphisms, and involutions: a computer solution to an open problem. I

Authors: S. K. Winker, L. Wos and E. L. Lusk
Journal: Math. Comp. 37 (1981), 533-545
MSC: Primary 20M15; Secondary 03B35, 20-04, 68G20
MathSciNet review: 628714
Full-text PDF Free Access

Abstract | References | Similar Articles | Additional Information

Abstract: An antiautomorphism H of a semigroup S is a 1-1 mapping of S onto itself such that $ H(xy) = H(y)H(x)$ for all x, y in S. An antiautomorphism H is an involution if $ {H^2}(x) = x$ for all x in S. In this paper the following question is answered: Does there exist a finite semigroup with antiautomorphism but no involution? This question, suggested by I. Kaplansky, was answered in the affirmative with the aid of an automated theorem-proving program. More precisely, there are exactly four such semigroups of order seven and none of smaller order. The program was a completely general one, and did not calculate the solution directly, but rather rendered invaluable assistance to the mathematicians investigating the question by helping to generate and examine various models. A detailed discussion of the approach is presented, with the intention of demonstrating the usefulness of a theorem prover in carrying out certain types of mathematical research.

References [Enhancements On Off] (What's this?)

  • [1] C. L. Chang & R. C. T. Lee, Symbol Logic and Mechanical Theorem Proving, Academic Press, New York, 1973. MR 0441028 (55:13894)
  • [2] D. E. Knuth & P. B. Bendix, "Simple word problems in universal algebras," Computational Problems in Abstract Algebras (J. Leech, Ed.), Pergamon Press, New York, 1970, pp. 263-297. MR 0255472 (41:134)
  • [3] J. D. McCharen, R. A. Overbeek & L. Wos, "Complexity and related enchancements for automated theorem-proving programs," Comput. Math. Appl., v. 2, 1976, pp. 1-16.
  • [4] J. D. McCharen, R. A. Overbeek & L. Wos, "Problems and experiments for and with automated theorem-proving programs," IEEE Trans. Comput., v. C-25, No. 8, 1976, pp. 773-782.
  • [5] R. A. Overbeek, "An implementation of hyper-resolution," Comput. Math. Appl., v. 1, 1975, pp. 201-214. MR 0386373 (52:7227)
  • [6] S. Winker & L. Wos, Automated Generation of Models and Counterexamples and Its Application to Open Questions in Ternary Boolean Algebra, Proc. 8th Internat. Sympos. on Multiple-Valued Logic, Rosemont, Illinois, May 1978, IEEE, New York and ACM, New York, pp. 251-256.

Similar Articles

Retrieve articles in Mathematics of Computation with MSC: 20M15, 03B35, 20-04, 68G20

Retrieve articles in all journals with MSC: 20M15, 03B35, 20-04, 68G20

Additional Information

Keywords: Finite semigroups, involutions, antiautomorphisms, automated theoremproving
Article copyright: © Copyright 1981 American Mathematical Society

American Mathematical Society