ausblenden:
Schlagwörter:
-
Zusammenfassung:
Cancellative superposition is a refutationally complete
calculus for first-order equational theorem proving in the
presence of the axioms of cancellative abelian monoids, and,
optionally, the torsion-freeness axioms. Thanks to strengthened
ordering restrictions, cancellative superposition avoids some
of the inefficiencies of classical AC-superposition calculi.
We show how the efficiency of cancellative superposition can
be further improved by using variable elimination techniques,
leading to a significant reduction of the number of variable
overlaps. In particular, we demonstrate that in divisible
torsion-free abelian groups, variable overlaps, AC-unification
and AC-orderings can be avoided completely.
