TY - JOUR
T1 - Quantifier elimination for modules with scalar variables
AU - van den Dries, Lou
AU - Holly, Jan
PY - 1992/5/25
Y1 - 1992/5/25
N2 - Van den Dries, L. and J. Holly, Quantifier elimination for modules with scalar variables, Annals of Pure and Applied Logic 57 (1992) 161-179. We consider modules as two-sorted structures with scalar variables ranging over the ring. We show that each formula in which all scalar variables are free is equivalent to a formula of a very simple form, uniformly and effectively for all torsion-free modules over gcd domains (=Bezout domains expanded by gcd operations). For the case of Presburger arithmetic with scalar variables the result takes a still simpler form, and we derive in this way the polynomial-time decidability of the sets defined by such formulas.
AB - Van den Dries, L. and J. Holly, Quantifier elimination for modules with scalar variables, Annals of Pure and Applied Logic 57 (1992) 161-179. We consider modules as two-sorted structures with scalar variables ranging over the ring. We show that each formula in which all scalar variables are free is equivalent to a formula of a very simple form, uniformly and effectively for all torsion-free modules over gcd domains (=Bezout domains expanded by gcd operations). For the case of Presburger arithmetic with scalar variables the result takes a still simpler form, and we derive in this way the polynomial-time decidability of the sets defined by such formulas.
UR - http://www.scopus.com/inward/record.url?scp=38249013186&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=38249013186&partnerID=8YFLogxK
U2 - 10.1016/0168-0072(92)90025-U
DO - 10.1016/0168-0072(92)90025-U
M3 - Article
AN - SCOPUS:38249013186
SN - 0168-0072
VL - 57
SP - 161
EP - 179
JO - Annals of Pure and Applied Logic
JF - Annals of Pure and Applied Logic
IS - 2
ER -