Difference between revisions of "Quantifier Elimination"

From redlog.eu
Jump to: navigation, search
m
 
(7 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:
<p>
 
* 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>.
 
<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 <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>.
+
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>
  
* [[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>.
+
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>

Qe-example.png


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

References

  • The Redlog Homepage [1]