Real quantifier elimination traditionally refers to eliminating
quantified variables from *Tarski formulas*, which are
boolean combinations of polynomial equalities and inequalities.
The atomic formulas in a Tarski formula in the variables
*x _{1}, ..., x_{k}* have the form

The language of *Extended Tarski formulas* (ETFs) is defined in
Chapter 7 of my
thesis, and it is shown that we can perform quantifier
elimination in this language using CADs - in fact it isn't really
different than quantifier elimination for Tarski formulas using
CADs. That chapter also formally defines the class of
*Restricted ETFs* and this language, which is still a
superset of the language of Tarski formulas, is the language of
input and output formulas in QEPCAD. Here we only give an
informal definition.

The language of Restricted ETFs extends the language of Tarski
formulas by allowing atomic formulas of the form
*x _{k} s root_{j}f(x_{1}, ..., x_{k})*,
where

`[ x2 > _root_1 x1^2 + x2^2 - 1 ]` |
A simple example in the extended language - the cells colored blue are in the set defined by the formula | |

```
[ x2 > _root_-2 (x1^2 + x2^2)^4 -
7 x1^6 x2 + 35 x1^4 x2^3 -
21 x1^2 x2^5 + x2^7 ]
``` |
Sometimes the sets defined by indexed root expressions are a bit odd! |

Christopher W Brown Last modified: Wed Jul 31 09:34:04 EDT 2002