** Next:** A short history of
** Up:** An Introduction to Quantifier
** Previous:** An Introduction to Quantifier

#

The quantifier elimination problem

The underlying problem motivating my research is the quantifier
elimination problem for the first order theory of real closed fields.
The variables of a formula in the theory of real closed fields are
elements of some real closed field, and the atomic formulas are sign
conditions on polynomials in those variables. Given a formula ,
the * quantifier elimination problem* asks for a formula
in which no variables are quantified such that
. is called the input
formula, and the solution formula.
An example of a simple and familiar quantifier elimination problem
input formula is:

One solution formula for this quantifier elimination problem is:

The input formula is in some sense asking the question: * When
does a quadratic polynomial have a real root?* The output formula
answers this question.
Many mathematical problems can be phrased as quantifier elimination
problems -- problems in real geometry, for example, or stability
problems in systems of differential equations as in
[Hong et al.(1997)Hong, Liska, and Steinberg] , or robot motion planning as in
[Schwartz and Sharir(1981)]. Its wide range of applicability would make an
efficient quantifier elimination method a very important tool.
However, as one might expect for so general a problem, quantifier
elimination is very difficult computationally.

** Next:** A short history of
** Up:** An Introduction to Quantifier
** Previous:** An Introduction to Quantifier
*Christopher W Brown*

*2001-07-10*