@article{Waldmann2002aJSC,
TITLE = {Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part I)},
AUTHOR = {Waldmann, Uwe},
LANGUAGE = {eng},
ISSN = {0747-7171},
LOCALID = {Local-ID: C1256104005ECAFC-0FE819BCE345C3C0C1256CAE005B3962-Waldmann2002aJSC},
YEAR = {2002},
DATE = {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 = {Journal of Symbolic Computation},
VOLUME = {33},
PAGES = {777--829},
}