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 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 (1)Basic Examples (1)

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[2]:=
Click for copyable input
Out[2]=

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

In[3]:=
Click for copyable input
Out[3]=
New in 5
New to Mathematica? Find your learning path »
Have a question? Ask support »