Documentation

Mathematica

The Mathematica Book

Mathematica Reference Guide

Experimental Context Objects in Mathematica 4

Experimental`Resolve

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.