We employ automated deduction techniques to prove and generalize some well-known theorems in group theory that involve power maps, i.e., functions of the form \(f(x) = x^n\) . The main difficulty is that if n is interpreted as an integer variable, then the results are not expressible in first-order logic of groups or semigroups, and hence not provable by modern first-order theorem provers. Here we demonstrate that an appropriate reformulation of power maps makes some basic mathematical concepts like GCD and mathematical induction accessible to the first-order automated theorem proving, allowing even for generalizations of the classical commutativity theorems in (semi)group theory.
