CancellativeAbelianMonoids and Related Structures in Refutational Theorem Proving (Part I)

We present superposition calculi in which the axioms of cancellativeAbelianmonoids and, optionally, the torsion-freeness axiom are integrated. CancellativeAbelianmonoids comprise Abelian groups, but also such ubiquitous structures as the natural numbers or multisets. Our calculi require neither extended clauses nor explicit inferences with the theory axioms. Compared with AC-superposition calculi, the number of variable overlaps is significantly reduced by strong ordering restrictions.