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

Waldmann, Uwe

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Report

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

MPS-Authors

/persons/resource/persons45689

Waldmann, Uwe
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

MPI-I-1999-2-003.pdf
(Any fulltext), 304KB

Supplementary Material (public)

There is no public supplementary material available

Citation

Waldmann, U.(1999). Cancellative superposition decides the theory of divisible torsion-free abelian groups (MPI-I-1999-2-003). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-6F75-5

Abstract

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.