Skip to Main Content

Mathematics of Computation

Published by the American Mathematical Society since 1960 (published as Mathematical Tables and other Aids to Computation 1943-1959), Mathematics of Computation is devoted to research articles of the highest quality in computational mathematics.

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

The 2020 MCQ for Mathematics of Computation is 1.78.

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