# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### Superposition for Divisible Torsion-Free Abelian Groups

##### Locator

There are no locators available

##### Fulltext (public)

There are no public fulltexts available

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Waldmann, U. (1998). Superposition for Divisible Torsion-Free Abelian Groups. In C.
Kirchner, & H. Kirchner (*Proceedings of the 15th
International Conference on Automated Deduction (CADE-98)* (pp. 144-159). Berlin, Germany: Springer.

Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-3894-C

##### Abstract

Variable overlaps are one of the main sources for the inefficiency of AC or ACU
theorem proving calculi. In the presence of the axioms of abelian groups or at
least cancellative abelian monoids, ordering restrictions allow us to avoid
some of these overlaps, but inferences with unshielded variables remain
necessary. In divisible torsion-free abelian groups, for instance the rational
numbers, every clause can be transformed into an equivalent clause without
unshielded variables. We show how such a variable elimination algorithm can be
integrated into the cancellative superposition calculus. The resulting calculus
is refutationally complete with respect to the axioms of divisible torsion-free
abelian groups and allows us to dispense with variable overlaps altogether. If
abstractions are performed eagerly, the calculus makes it furthermore possible
to avoid the computation of AC unifiers and AC orderings.