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
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
- 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.
Additional Information
- © Copyright 1981 American Mathematical Society
- 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