- quantified formula in prenex form over a real field:

where is a general quantifier (for all) or existential quantifier (there exists) and is a logical combination of polynomial equations and inequalities in the variables

- variables are free (not quantified) and variables are quantified
- there exists a quantifier free formula in free
variables which is equivalent to the
formula
- quantifier elimination is the procedure which transforms the quantified
formula into the quantifier free formula
- around 1930 Tarski proved that quantifier elimination is possible
- first quantifier elimination method was proposed by Tarski 1951,
however its complexity cannot be bound by any tower of exponentials
- cylindrical algebraic decomposition method by Collins 1975
made a breakthrough having ``only'' double exponential complexity
- improvements in the method of partial cylindrical algebraic decomposition:
Collins and Hong 1991, programm QEPCAD
- example: the quantified formula

- is equivalent to the quantifier free formula

Richard Liska