Item

Abstract

Cancellative abelian monoids encompass abelian groups,
but also such ubiquitous structures as the natural numbers or
multisets. Both the AC axioms and the cancellation law are
difficult for a general purpose theorem prover, as they create
many variants of clauses which contain sums. We describe a
refined superposition calculus for cancellative abelian monoids
which requires neither explicit inferences with the theory clauses
nor extended equations or clauses. Strong ordering constraints
allow us to restrict to inferences that involve the maximal term
of the maximal sum in the maximal literal. Besides, the search
space is reduced drastically by variable elimination techniques.