Department of Mathematics
Server

The Baer-Alperin theorem says that a torsion-free group in which the power map \( f(x) = x^n \) for some \( n \ge 2 \) is a homorphism is abelian. In this talk, we employ automated deduction techniques to prove and generalize this to cancellative semigroups. The difficulty lies in the fact that the term \( x^n \) cannot be expressed in the syntax of first-order logic when n is an integer variable. Here we describe a new concept of "power-like function" by extracting relevant equational properties valid for all power functions and implement these rules in Prover9, a first-order theorem-prover developed by Dr. William McCune. Now we recast the original theorems and prove them in this new context of power-like functions. Prover9, enriched with these rules, now proves these new theorems. Consequently these first-order proofs remain valid for all n but the length and complexity of the proofs remain constant independent of the value of n. For example, we show that every torsion-free group in which a power-like map is an endomorphism is abelian. Also, we generalize such theorems for the class of all cancellative semigroups, and once again, Prover9 happily proves all these new generalizations as well. This research was done in collaboration with G.I. Moghaddam and Yang Zhang.

References:

1. J. L. Alperin, A classification of n-abelian groups, Can. J. Math., 21, (1969).
2. R. Baer, Factorization of \( n \)-soluble and \( n \)-nilpotent groups, Proc. Amer. Math. Soc., 4, 15-26 (1953).
3. G.I. Moghaddam, R. Padmanabhan and Yang Zhang, Automated Reasoning with Power-Maps (to appear).