Q E P C A D - What is Quantifier Elimination?
An Informal Descriptionthere exists an x such that a x2 + b x + c = 0 and a /= 0
quantifier elimination should produce an equivalent formula like
a /= 0 and 4 a c - b2 <= 0
The quantified variable x has been eliminated.
In essence, the quantified input formula is a question, "When
does there exist an x such that ...?", and the
quantifier-free equivalent formula is an answer, "There exists
sich an x when ...".
interesting problems in a wide variety of disciplines can be
phrased as quantifier elimination problems. Now, how many of
the really interesting problems can be solved in a reasonable
amount of time by todays software is another question ...
Informally, the quantifier elimination problem is this: Given a boolean combination of
equalities and inequalities of polynomials with integer coefficients in which some
variables appear quantified, produce an equivalent formula in
which no quantified variables appear (all variables are
assumed to be real).
For example, if the input formula is
Quantifier Elimination Algorithms
Quantifier elimination by CAD is one algorithm for QE. There
are others, and in the future this section will describe some of
them and point you to other systems for QE.
Christopher W Brown
Last modified: Wed Jul 31 09:48:51 EDT 2002