Figure 3. Functions related to quantifier elimination.
The following proves that circles and do not intersect. The inequality assumption is interpreted such that x and y are real and they satisfy the inequality.
The next example finds a necessary and sufficient condition for a quadratic to have real roots. Note that we need to assume that all variables are real.
Here is a more complicated condition for a monic quartic to have real roots.
Resolve we can find the values of
a for which inequalities
i2[a] defined in the section "Decision Problem" have common solutions.
Resolve can be used on expressions containing several quantifiers. Here we compute the limit of a rational function at infinity using the definition of limit.
Resolve with one argument uses the linear quantifier elimination algorithm of Loos and Weispfenning whenever possible. In this case the result will be a system of algebraic equations and inequalities in the free variables; however, the system may not be in the cylindrical solution form. The advantage of the linear quantifier elimination algorithm is that it depends on the number of free variables only as much as the basic polynomial arithmetic does, compared to the doubly exponential dependence of the cylindrical algebraic decomposition algorithm.
This eliminates the quantifier from
F quickly; however, the solution is given in an implicit form.
Here we get the solution in the cylindrical solution form. However, the computation takes longer.
Converted by Mathematica
April 24, 2000
[Prev Page][Next Page]