The Mathematica Journal
Departments
Feature Articles
Columns
New Products
New Publications
Classifieds
Calendar
News Bulletins
Mailbox
Letters
Write Us
About the Journal
Staff and Contributors
Submissions
Subscriptions
Advertising
Back Issues
Home
Download this Issue

Quantifier Elimination

[Graphics:../Images/index_gr_98.gif] [Graphics:../Images/index_gr_99.gif]
[Graphics:../Images/index_gr_100.gif] [Graphics:../Images/index_gr_101.gif]
[Graphics:../Images/index_gr_102.gif] [Graphics:../Images/index_gr_103.gif]
[Graphics:../Images/index_gr_104.gif] [Graphics:../Images/index_gr_105.gif]

Figure 3. Functions related to quantifier elimination.

The following proves that circles [Graphics:../Images/index_gr_106.gif] and [Graphics:../Images/index_gr_107.gif] do not intersect. The inequality assumption [Graphics:../Images/index_gr_108.gif] is interpreted such that x and y are real and they satisfy the inequality.

[Graphics:../Images/index_gr_109.gif]
[Graphics:../Images/index_gr_110.gif]

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.

[Graphics:../Images/index_gr_111.gif]
[Graphics:../Images/index_gr_112.gif]

Here is a more complicated condition for a monic quartic to have real roots.

[Graphics:../Images/index_gr_113.gif]
[Graphics:../Images/index_gr_114.gif]

Using Resolve we can find the values of a for which inequalities i1[a] and i2[a] defined in the section "Decision Problem" have common solutions.

[Graphics:../Images/index_gr_115.gif]
[Graphics:../Images/index_gr_116.gif]

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.

[Graphics:../Images/index_gr_117.gif]
[Graphics:../Images/index_gr_118.gif]

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.

[Graphics:../Images/index_gr_119.gif]

This eliminates the quantifier from F quickly; however, the solution is given in an implicit form.

[Graphics:../Images/index_gr_120.gif]
[Graphics:../Images/index_gr_121.gif]

Here we get the solution in the cylindrical solution form. However, the computation takes longer.

[Graphics:../Images/index_gr_122.gif]
[Graphics:../Images/index_gr_123.gif]

Converted by Mathematica      April 24, 2000

[Article Index] [Prev Page][Next Page]