Q E P C A D - What is Quantifier Elimination?

An Informal Description
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

there 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 ...". Lots of 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 ...

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