On delineability of varieties in CAD-based quantifier elimination with two equational constraints

摘要

Let V ? Rr denote the real algebraic variety defined by the conjunction f = 0 ∧ g = 0, where f and g are real polynomials in the variables x1, ..., xr and let S be a submanifold of Rr-2. This paper proposes the notion of the analytic delineability of V on S with respect to the last 2 variables. It is suggested that such a notion could be useful in solving more efficiently certain quantifier elimination problems which contain the conjunction f = 0 ? g = 0 as subformula, using a variation of the CAD-based method. Two bi-equational lifting theorems are proved which provide the basis for such a method.