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

DOI:
https://doi.org/10.1090/S0025-5718-1981-0628714-5

MathSciNet review:
628714

Full-text PDF

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 for all *x, y* in *S*. An antiautomorphism *H* is an *involution* if 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.

**[1]**Chin Liang Chang and Richard Char Tung Lee,*Symbolic logic and mechanical theorem proving*, Academic Press, New York-London, 1973. Computer Science and Applied Mathematics. MR**0441028****[2]**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****[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]**Ross A. Overbeek,*An implementation of hyper-resolution*, Comput. Math. Appl.**1**(1975), no. 2, 201–214. MR**0386373**, https://doi.org/10.1016/0898-1221(75)90019-X**[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.

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

DOI:
https://doi.org/10.1090/S0025-5718-1981-0628714-5

Keywords:
Finite semigroups,
involutions,
antiautomorphisms,
automated theoremproving

Article copyright:
© Copyright 1981
American Mathematical Society