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 elauses nor explicit inferences with the theory axioms. Compared with AC-superposition calculi, the number of variable overlaps is significantly reduced by strong ordering restrictions.
展开▼
