Paramodulation with Built-In Abelian Groups

A new technique is presented for superposition with firstorder clauses with built-in abelian groups (AG). Compared with previous approaches, it is simpler, and no inferences with the AG axioms or abstraction rules are needed. Furthermore, AG-unification is used instead of the computationally more expensive unification modulo associativity and commutativity. Due to the simplicity and restrictiveness of our inference system, its compatibility with redundancy notions and constraints, and the fact that standard term orderings like RPO can be used, we believe that our technique will become the method of choice for practice, as well as a basis for new theoretical developments like logicbased complexity and decidability analysis. Keywords: term rewriting, automated deduction. 1 Introduction It is crucial for the performance of a deduction system that it incorporates specialized techniques to work efficiently with standard algebraic theories, since a nave handling of some axioms (like assoc..