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

Cancellative superposition is a refutationally complete calculus for first-order equational theorem proving in the presence of the axioms of cancellativeAbelianmonoids, and, optionally, the torsion-freeness axioms. Thanks to strengthened ordering restrictions, cancellative superposition avoids some of the inefficiencies of classical AC-superposition calculi. We show how the efficiency of cancellative superposition can be further improved by using variable elimination techniques, leading to a significant reduction of the number of variable overlaps. In particular, we demonstrate that in divisible torsion-free Abelian groups, variable overlaps, AC-unification and AC-orderings can be avoided completely.