非表示:
キーワード:
-
要旨:
We present a constraint superposition calculus in which the axioms of
cancellative abelian monoids and, optionally, further axioms (e.g.,
torsion-freeness) are integrated. Cancellative abelian monoids comprise abelian
groups, but also such ubiquitous structures as the natural numbers or
multisets. Our calculus requires neither extended clauses nor explicit
inferences with the theory axioms. The number of variable overlaps is
significantly reduced by strong ordering restrictions and powerful variable
elimination techniques; in divisible torsion-free abelian groups, variable
overlaps can even be avoided completely. Thanks to the equivalence of
torsion-free cancellative and totally ordered abelian monoids, our calculus
allows us to solve equational problems in totally ordered abelian monoids
without requiring a detour via ordering literals.
