Cancellative superposition decides the theory of divisible torsion-free abelian groups

In divisible torsion-free abelian groups, the efficiency of the cancellative superposition calculus can be greatly increased by combining it with a variable elimination algorithm that transforms every clause into an equivalent clause without unshielded variables. We show that the resulting calculus is a decision procedure for the theory of divisible torsion-free abelian groups. (orig.)Available from TIB Hannover: RR 1912(1999-2-003) / FIZ - Fachinformationszzentrum Karlsruhe / TIB - Technische InformationsbibliothekSIGLEDEGerman