Skip to Main Content

Mathematics of Computation

Published by the American Mathematical Society, the Mathematics of Computation (MCOM) is devoted to research articles of the highest quality in all areas of pure and applied mathematics.

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

The 2020 MCQ for Mathematics of Computation is 1.98.

What is MCQ? The Mathematical Citation Quotient (MCQ) measures journal impact by looking at citations over a five-year period. Subscribers to MathSciNet may click through for more detailed information.


Semigroups, antiautomorphisms, and involutions: a computer solution to an open problem. I
HTML articles powered by AMS MathViewer

by S. K. Winker, L. Wos and E. L. Lusk PDF
Math. Comp. 37 (1981), 533-545 Request permission


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.
  • Chin Liang Chang and Richard Char Tung Lee, Symbolic logic and mechanical theorem proving, Computer Science and Applied Mathematics, Academic Press, New York-London, 1973. MR 0441028
  • Donald E. Knuth and Peter B. Bendix, Simple word problems in universal algebras, Computational Problems in Abstract Algebra (Proc. Conf., Oxford, 1967) Pergamon, Oxford, 1970, pp. 263–297. MR 0255472
  • 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. 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.
  • Ross A. Overbeek, An implementation of hyper-resolution, Comput. Math. Appl. 1 (1975), no. 2, 201–214. MR 386373, DOI 10.1016/0898-1221(75)90019-X
  • 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
Additional Information
  • © Copyright 1981 American Mathematical Society
  • Journal: Math. Comp. 37 (1981), 533-545
  • MSC: Primary 20M15; Secondary 03B35, 20-04, 68G20
  • DOI:
  • MathSciNet review: 628714