BUILT-IN MATHEMATICA 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 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:

 Out[1]=

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

 Out[2]=

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

 Out[3]=