Local quantifier elimination
Andreas Dolzmann, Volker Weispfenning · 2000
We introduce local quantifier elimination as a new variant of real quantifier elimination. Given a first-order formula and a real point we compute a quantifier-free formula which is not only for the given point equivalent to the input formula but also for all points in a semi-algebraic set containing the specified point. The description of this semi-algebraic set is explicitly computed in the form of a conjunction of atomic formulas. Local quantifier elimination is in its application area superior to both regular and generic quantifier elimination due to faster running times and shorter results.