This is documentation for Mathematica 6, which was
based on an earlier version of the Wolfram Language.
View current documentation (Version 11.1)


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.
New in 5