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.

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 principles always eliminate quantifiers for any Boolean expression expr.

Prove that the unit disk is nonempty:

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

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