Difference between revisions of "Quantifier Elimination"
From redlog.eu
Thomas-sturm (Talk | contribs) |
Thomas-sturm (Talk | contribs) |
||
| Line 2: | Line 2: | ||
To get an idea consider the following illustrating example over the real numbers: | 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: <math>f(x,y)=x^2+xy+b</math> and <math>g(x,y)=x+ay^2+b</math>. | * Consider two bivariate polynomials with parameters a and b over the reals: <math>f(x,y)=x^2+xy+b</math> and <math>g(x,y)=x+ay^2+b</math>. | ||
| − | + | ||
* 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 <math>f(x,y)>0</math> and <math>g(x,y)\leq0</math>. | * 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 <math>f(x,y)>0</math> and <math>g(x,y)\leq0</math>. | ||
Revision as of 21:31, 23 April 2009
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: <math>f(x,y)=x^2+xy+b</math> and <math>g(x,y)=x+ay^2+b</math>.
- 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 <math>f(x,y)>0</math> and <math>g(x,y)\leq0</math>.
- The problem can be straightforwardly formulated as a first-order formula: <math>\varphi=\forall x\exists y(x^2+xy+b>0 \land x+ay^2+b\leq0)</math>.
- REDLOG's quantifier elimintion delivers within half a second necessary and sufficient conditions, which are obviously equivalent to <math> a<0\land b>0</math>.
A comprehensive collection of Redlog examples can be found in the REMIS online database.
References
- The Redlog Homepage [1]
