next up previous
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 $F$, the quantifier elimination problem asks for a formula ${\overline F}$ in which no variables are quantified such that ${\overline F} \Longleftrightarrow F$. $F$ is called the input formula, and ${\overline F}$ the solution formula.

An example of a simple and familiar quantifier elimination problem input formula is:

\begin{displaymath}
F: (\exists x)[ a x^2 + b x + c = 0 ]
\end{displaymath}

One solution formula for this quantifier elimination problem is:

\begin{displaymath}
{\overline F}: b^2 - 4 a c \geq 0 \hspace{0.1 in} \wedge \hs...
...ce{0.1 in}a \neq 0
\hspace{0.1 in} \vee \hspace{0.1 in}c = 0 ]
\end{displaymath}

The input formula $F$ is in some sense asking the question: When does a quadratic polynomial have a real root? The output formula ${\overline F}$ 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 up previous
Next: A short history of Up: An Introduction to Quantifier Previous: An Introduction to Quantifier
Christopher W Brown
2001-07-10