# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

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

##### Fulltext (public)

There are no public fulltexts stored in PuRe

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Waldmann, U. (1997). A Superposition Calculus for Divisible Torsion-Free Abelian Groups.
In M. P. Bonacina, & U. Furbach (*Proceedings of
the International Workshop on First-Order Theorem Proving (FTP-97)* (pp. 130-134). Linz, Austria: Johannes Kepler
Universität.

Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-39D3-3

##### 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.