Wolfram Research, Inc.
Resolve[expr] attempts to eliminate quantifiers in expr.
Resolve handles quantifiers of the form Exists[x, condition, expr] and ForAll[x, condition, expr].
Exists[x, c, expr] can be input in the form .
ForAll[x, c, expr] can be input in the form .
Lists of variables can be used in Exists and ForAll.
The algorithms of Resolve are used automatically inside FullSimplify.
See also: CylindricalAlgebraicDecomposition, FullSimplify.
Note: this is an experimental feature, and in future versions of Mathematica it may not be supported, or may have a different specification.