Superposition with completely built-in Abelian groups

A new technique is presented for superposition with first-order clauses with built-in Abelian groups (AG). Compared with previous approaches, it is simpler, and AG-unification is used instead of the computationally more expensive unification modulo associativity and commutativity. Furthermore, no inferences with the AG axioms or abstraction rules are needed; in this sense this is the first approach where AG is completely built in.