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.

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.

See Section 3.4.11.

Implementation Notes: see Section A.9.5.

See also: Reduce, FindInstance, Exists, ForAll.

New in Version 5.0.

Further Examples