非表示:
キーワード:
-
要旨:
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.
