# Wolfram Language & System 10.4 (2016)|Legacy Documentation

This is documentation for an earlier version of the Wolfram Language.
BUILT-IN WOLFRAM LANGUAGE SYMBOL

# 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==rhs equations lhs!=rhs inequations or inequalities expr∈dom domain specifications {x,y,…}∈reg region 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]:=
 Out[1]=

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

 In[1]:=
 Out[1]=

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

 In[1]:=
 Out[1]=

Find the projection of a geometric region:

 In[1]:=
 Out[1]=
 In[2]:=
 Out[2]=