BUILT-IN MATHEMATICA SYMBOL
Resolve
Resolve[expr]
attempts to resolve expr into a form that eliminates ForAll and Exists quantifiers.
- 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.
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]= |  |
New in 5
