# Difference between revisions of "Quantifier Elimination"

From redlog.eu

Thomas-sturm (Talk | contribs) |
Thomas-sturm (Talk | contribs) m |
||

(6 intermediate revisions by one user not shown) | |||

Line 1: | Line 1: | ||

− | Quantifier elimination is implemented in the [[REDUCE]] [[Packages|package]] [[Redlog]]. | + | Quantifier elimination is implemented in the [[REDUCE]] [[:Category:Packages|package]] [[Redlog]]. |

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,\quad 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,\quad 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> | |

+ | <p> | ||

[[image:qe-example.png|center]] | [[image:qe-example.png|center]] | ||

+ | <br> | ||

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

− | =References= | + | ==References== |

* The Redlog Homepage [http://www.redlog.eu] | * The Redlog Homepage [http://www.redlog.eu] | ||

+ | |||

+ | [[Category:Mathematics]] |

## Latest revision as of 20:52, 26 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,\quad 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,\quad 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]