Resolve

Resolve[expr]
attempts to resolve expr into a form that eliminates ForAll and Exists quantifiers.

Resolve[expr,dom]
works over the domain dom. Common choices of dom are Complexes, Reals, and Booleans.

Details and OptionsDetails and Options

  • Resolve is in effect automatically applied by Reduce.
  • expr can contain equations, inequalities, domain specifications, and quantifiers, in the same form as in Reduce.
  • The statement expr can be any logical combination of:
  • lhs==rhsequations
    lhs!=rhsinequations
    or inequalities
    exprdomdomain specifications
    {x,y,}regregion specification
    ForAll[x,cond,expr]universal quantifiers
    Exists[x,cond,expr]existential quantifiers
  • The result of Resolve[expr] always describes exactly the same mathematical set as expr, but without quantifiers.
  • Resolve[expr] assumes by default that quantities appearing algebraically in inequalities are real, while all other quantities are complex.
  • When a quantifier such as ForAll[x,] is eliminated, the result will contain no mention of the localized variable x.
  • Resolve[expr] can in principle always eliminate quantifiers if expr contains only polynomial equations and inequalities over the reals or complexes.
  • Resolve[expr] can in principle always eliminate quantifiers for any Boolean expression expr.

ExamplesExamplesopen allclose all

Basic Examples  (4)Basic Examples  (4)

Prove that the unit disk is nonempty:

In[1]:=
Click for copyable input
Out[1]=

Find the conditions for a quadratic form over the reals to be positive:

In[1]:=
Click for copyable input
Out[1]=

Find conditions for a quadratic to have at least two distinct complex roots:

In[1]:=
Click for copyable input
Out[1]=

Find the projection of a geometric region:

In[1]:=
Click for copyable input
Out[1]=
In[2]:=
Click for copyable input
Out[2]=
Introduced in 2003
(5.0)
| Updated in 2014
(10.0)