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