Journal of Symbolic Computation, 33(6):777-829, June 1, 2002.
Abstract: We present superposition calculi in which the axioms of cancellative abelian monoids and, optionally, the torsion-freeness axiom are integrated. Cancellative abelian monoids 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.
Journal of Symbolic Computation, 33(6):831-861, June 1, 2002.
Abstract: Cancellative superposition is a refutationally complete calculus for first-order equational theorem proving in the presence of the axioms of cancellative abelian monoids, 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.