Eliminace kvantifikátorů

• kvantifikovaný vzorec v prenex tvaru v oboru reálných čísel
  
  $$G= (Q_{f+1} x_{f+1}) \ldots (Q_r x_r) F(x_1,\ldots,x_r)$$
  
  

• kde Qi je obecný kvantifikátor (pro všechna) nebo existenční kvantifikátor (existuje) a F je logická kombinace polynomiálních rovnic a nerovnic v proměnných x₁,...,x_r

• f proměnných je volných (nejsou kvantifikovány) a r - f proměnných je kvantifikovaných

• existuje nekvantifikovaný vzorec H ve volných proměnných x₁,...,x_f ekvivalentní vzorci G

• eliminace kvantifikátorů je proces, který z kvantifikovaného vzorce G najde nekvantifikovaný vzorec H

• první metodu pro eliminaci kvantifikátorů navrhl Tarski

• metoda válcové algebraické dekomposice, Collins 1975

• zlepšení v metodě částečné válcové algebraické dekomposice, Collins a Hong 1991; program QEPCAD

• příklad; kvantifikovaný vzorec
  
  $$\begin{eqnarray*}(\forall S_1)&(\forall S_2)& (C > 0) \land\\ &&[ ( 0 \leq S_1 ... ... S_2 C^2 + S_1 C^2\\ &&-2 S_1 C + S_2 C^2 - 2 S_2 C + 1 \geq 0] \end{eqnarray*}$$
  
  

• je ekvivalentní nekvantifikovanému vzorci
  
  $$0 < C \leq \frac{1}{2}$$