Superposition Theorem Proving for Commutative Algebraic Theories

We develop special superposition calculi for first-order theorem proving in the theories of abelian groups, commutative rings, and modules and commutative algebras over fields or over the ring of integers, in order to make automated theorem proving in these theories more effective. The calculi are refutationally complete on arbitrary sets of ground clauses, which in particular may contain additional function symbols. The calculi are derived systematically from a representation of the theory as a convergent term rewriting system. Compared to standard superposition they have stronger ordering restrictions so that inferences are applied only to maximal summands, and they contain macro inference rules that use theory axioms in a goal directed fashion. In general we need additional inferences to handle critical peaks between extended clauses. We show that these are not needed for abelian groups and modules, and that for commutative rings and commutative algebras one such inference suffices for any pair of ground clauses. To facilitate the construction of term orderings for such calculi we introduce theory path orderings