Resolve
関数Resolveは関数Reduceと同じ方法を使って，複素変数あるいは実変数の任意の多項式系から量限定子（例えば， および  等）を除去することができます．明示的な解を計算するよりも，系の陰的なquantifier-free形式を得る方が簡単な場合は，Resolveは陰形式を返します．また，Resolveはブール変数を含む量限定子を除去することもできます．
例：制約条件を満足する係数
以下で，実数変数の4次多項式が正になるために，実数係数a，b，c が満足しなければならない条件を与えます．
![Resolve[ [ForAll]_(x_1 {x_1 a_1 b_1 c} [ElementOf] R) c x^2 + b x + a [GreaterThan] 0]](images/resolve_3.gif "Resolve[ [ForAll]_(x_1 {x_1 a_1 b_1 c} [ElementOf] R) c x^2 + b x + a [GreaterThan] 0]")
![b < 0 [And] c > 0 [And] a > ((b^2)/(4c)) [Or] b == 0 [And] c [GreaterThanOrEqualTo] 0 [And] a > 0 [Or] b > 0 [And] c > 0 [And] a > ((b^2)/(4c)](images/resolve_4.gif "b < 0 [And] c > 0 [And] a > ((b^2)/(4c)) [Or] b == 0 [And] c [GreaterThanOrEqualTo] 0 [And] a > 0 [Or] b > 0 [And] c > 0 [And] a > ((b^2)/(4c)")
例：x2 + y2 < 1は，y > x4 - 2を意味しているか
![Resolve[ [ForAll]_(x_1 y} (x^2 + y^2 < 1 => y > x^4 - 2)](images/resolve_9.gif "Resolve[ [ForAll]_(x_1 y} (x^2 + y^2 < 1 => y > x^4 - 2)")
以下の図より，上の結果は単位円が双曲線の中に存在することを意味していることが分かります．
| 
![[en]](/common/images2003/lang_bottom_en.gif)