MPI-INF/SWS Research Reports 1991-2021
2. Number - All Departments
MPI-I-1999-2-003
Cancellative superposition decides the theory of divisible torsion-free abelian groups
Waldmann, Uwe
March 1999, 23 pages.
.Status: available - back from printing
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.
-
- Attachement: MPI-I-1999-2-003.ps (269 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1999-2-003
BibTeX@TECHREPORT{WaldmannMPI-I-1999-2-003,
AUTHOR = {Waldmann, Uwe},
TITLE = {Cancellative superposition decides the theory of divisible torsion-free abelian groups},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-1999-2-003},
MONTH = {March},
YEAR = {1999},
ISSN = {0946-011X},
}