Quantifier elimination

 

• 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
  
  

 
• Example with QEPCAD program