Quantifier Elimination

Many mathematical and industrial problems can be translated to formulas consisting of polynomial equations, inequalities, quantifiers ( $\forall, \exists$) and Boolean operators ( $\land, \lor, \lnot, \rightarrow, etc$). Such formulas construct sentences in the so-called first-order theory of real closed fields and are called first-order formulas.

Let $f_i(X,U) \in {\bf Q}[X,U]$, $i=1,2,\cdots,t,$ where Q is the fields of rational numbers, $X=(x_1,\cdots,x_n)$ $\in {\bf R}^n$ a vector of quantified variables, and $U=(u_1,\cdots,u_m)$ $\in {\bf R}^m$ a vector of unquantified parameter variables. Let $F_i = f_i(X,U) \ \Box_i \ 0$, where $\Box_i \in \{ =,\geq,>,\ne \}$, for $i=1,\cdots,s$, $Q_j \in \{ \forall, \exists \},$ and X_j a block of q_j quantified variables for $j=1,\cdots,s$. In general, quantified formula $\varphi$ is given

$$\varphi = {(^{Q_1}X_1 \cdots \ ^{Q_s}X_s)} \ G(F_1,\cdots,F_t)$$ (5)

where $G(F_1,\cdots,F_t)$ is a quantifier-free (qf) Boolean formula.

QE procedure is an algorithm to compute equivalent qf formula for a given first-order formula. If all variables are quantified, i.e. m=0, QE procedure decides whether the given formula (5) is true or false. This problem is called decision problem. When there are some unquantified variables U, QE procedure find a qf formula $\varphi(U)$ describing the range of possible U where $\varphi(U)$ is true. If there is no such range QE outputs false. This problem is called general quantifier elimination problem.

The history of the algorithms QE begins with Tarski-Seidenberg decision procedure in 1950's ([17],[14]). But this is intricate and far from feasible. In 1975, Collins presented a more efficient general purpose QE algorithm based on Cylindrical Algebraic Decomposition (CAD) [5]. The algorithm has improved by Collins and Hong in [6] and was implemented on SACLIB as ``QEPCAD'' by Hong. Weispfenning also presented a very efficient QE algorithm based on test terms [18],[19]. Though there is some degree restriction of a quantified variable in input formulas for this approach, it seems very practical. Implementation of the method was done on Reduce as ``REDLOG'' and Risa/Asir ¹ [13] by Sturm [15], [16]. Here we use both QE implementation on Risa/Asir and REDLOG.