hide
Free keywords:
Computer Science, Symbolic Computation, cs.SC,Computer Science, Logic in Computer Science, cs.LO
Abstract:
We generalize the framework of virtual substitution for real quantifier
elimination to arbitrary but bounded degrees. We make explicit the
representation of test points in elimination sets using roots of parametric
univariate polynomials described by Thom codes. Our approach follows an early
suggestion by Weispfenning, which has never been carried out explicitly.
Inspired by virtual substitution for linear formulas, we show how to
systematically construct elimination sets containing only test points
representing lower bounds.
