Sorry if any of this is unclear, or doesn't make much sense, I'm still trying to figure it out, a practical example such as this would likely help me understand better than anything else. I have read some articles about Tarski's proof of quantifier elimination for the reals, and I'm almost at the point of understanding the idea, although I'm still unclear how the algorithm works in practice, as in every source I found there were no examples. The basic idea of the algorithm was to use Sturm's ideas about counting roots, and creating lists of roots, and evaluating the signs on intervals of the real line.

For example, if I had the following statement

$\exists x. (ax^2 + bx + c > 0 \land dx + e > 0)$

According to one of the reference books I was looking at, putting this in quantifier free form involves listing the roots, i.e. if $p(x) = ax^2 + bx + c$ and $q(x) = dx + e$ then we could say e.g. $p(x)$ has roots $p_1, p_2$, where $p_1 < p_2$ and $q(x)$ has root $q_1$. There are three possible orderings assuming the roots are all distinct:

$p_1 < q_1 < p_2$

$p_1 < p_2 < q_1$

$q_1 < p_1 < p_2$

For each case, we can determine the truth of our original statement by evaluating the sign of $p(x)$ and $q(x)$ on the relevant intervals, e.g. in the first case,we evaluate the sign of $p(x)$ and $q(x)$ on the intervals $(-\infty, p_1), (p_1, q_1), (q_1, p_2), (p_2, \infty)$. I can see the relevance of this, but I don't really understand how this practically works to generate a quantifier free formula. Can anyone show how the algorithm actually would run in an example such as the one given? Even if someone could give an example of how the algorithm would run on a simpler example, such as $\exists x. ax^2 +bx + c > 0$, that would be helpful, as I can't really find any good worked examples. (Preferably not using CAD as I have no experience of it).

  • 2
    $\begingroup$ This is a comment, not an answer, because I'll just give a quantifier-free equivalent of $\exists x.ax^2+bx+c>0$, not run through the algorithm to get it. The desired formula is the disjunction of 4 cases: (1) $a>0$, (2) $a=0\land b\neq0$, (3) $a=0\land b=0\land c>0$, (4) $a<0\land b^2-4ac>0$. The algorithm would probably do a lot of work to get this, because it's deigned to work in general, not just for easy cases like this. The algorithm is, in general, very inefficient (double exponential), which is probably why you couldn't find examples worked out. $\endgroup$ – Andreas Blass Jul 23 at 1:34
  • $\begingroup$ reference.wolfram.com/language/ref/Resolve.html $\endgroup$ – Matt F. Jul 23 at 1:36
  • 1
    $\begingroup$ This is not a research-level question, so it probably belongs to math.stackexchange.com. For examples you should look up Cylindrical algebraic decomposition, such as this. $\endgroup$ – Andrej Bauer Jul 23 at 14:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.