# Difference between revisions of "Quantifier Elimination"

Quantifier elimination is implemented in the REDUCE package Redlog.

To get an idea consider the following illustrating example over the real numbers:

• Consider two bivariate polynomials with parameters a and b over the reals: $f(x,y)=x^2+xy+b$ and $g(x,y)=x+ay^2+b$.
<p>
• We are interested in necessary and sufficient conditions on the parameters a and b such that the following holds: For each real point x there exists some real point y such that $f(x,y)>0$ and $g(x,y)\leq0$.
• The problem can be straightforwardly formulated as a first-order formula: $\varphi=\forall x\exists y(x^2+xy+b>0 \land x+ay^2+b\leq0)$.
• REDLOG's quantifier elimintion delivers within half a second necessary and sufficient conditions, which are obviously equivalent to $a<0\land b>0$.

A comprehensive collection of Redlog examples can be found in the REMIS online database.

# References

• The Redlog Homepage [1]