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), 533545
MSC:
Primary 20M15; Secondary 03B35, 2004, 68G20
MathSciNet review:
628714
Fulltext PDF Free Access
Abstract 
References 
Similar Articles 
Additional Information
Abstract: An antiautomorphism H of a semigroup S is a 11 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 theoremproving 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, 1973. Computer Science and Applied Mathematics.
MR
0441028 (55 #13894)
 [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
(41 #134)
 [3]
J. D. McCharen, R. A. Overbeek & L. Wos, "Complexity and related enchancements for automated theoremproving programs," Comput. Math. Appl., v. 2, 1976, pp. 116.
 [4]
J. D. McCharen, R. A. Overbeek & L. Wos, "Problems and experiments for and with automated theoremproving programs," IEEE Trans. Comput., v. C25, No. 8, 1976, pp. 773782.
 [5]
Ross
A. Overbeek, An implementation of hyperresolution, Comput.
Math. Appl. 1 (1975), no. 2, 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 MultipleValued Logic, Rosemont, Illinois, May 1978, IEEE, New York and ACM, New York, pp. 251256.
 [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. 263297. MR 0255472 (41:134)
 [3]
 J. D. McCharen, R. A. Overbeek & L. Wos, "Complexity and related enchancements for automated theoremproving programs," Comput. Math. Appl., v. 2, 1976, pp. 116.
 [4]
 J. D. McCharen, R. A. Overbeek & L. Wos, "Problems and experiments for and with automated theoremproving programs," IEEE Trans. Comput., v. C25, No. 8, 1976, pp. 773782.
 [5]
 R. A. Overbeek, "An implementation of hyperresolution," Comput. Math. Appl., v. 1, 1975, pp. 201214. 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 MultipleValued Logic, Rosemont, Illinois, May 1978, IEEE, New York and ACM, New York, pp. 251256.
Similar Articles
Retrieve articles in Mathematics of Computation
with MSC:
20M15,
03B35,
2004,
68G20
Retrieve articles in all journals
with MSC:
20M15,
03B35,
2004,
68G20
Additional Information
DOI:
http://dx.doi.org/10.1090/S00255718198106287145
PII:
S 00255718(1981)06287145
Keywords:
Finite semigroups,
involutions,
antiautomorphisms,
automated theoremproving
Article copyright:
© Copyright 1981 American Mathematical Society
