BUILT-IN MATHEMATICA SYMBOL

Resolve

Resolve[expr]
attempts to resolve expr into a form that eliminates ForAll and Exists quantifiers.

Resolve

works over the domain dom. Common choices of dom are Complexes, Reals, and Booleans.

MORE INFORMATION

Resolve is in effect automatically applied by Reduce.

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

EXAMPLES

CLOSE ALL

Basic Examples (1)

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:

Prove that the unit disk is nonempty:

In[1]:=

Out[1]=

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

In[2]:=

Out[2]=

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

In[3]:=

Out[3]=

Scope (39)

Decide the existence of solutions of a univariate polynomial equation:

Decide the existence of solutions of a multivariate polynomial system:

Decide the truth value of fully quantified polynomial formulas:

Find conditions under which a polynomial equation has solutions:

Find conditions under which a polynomial system has solutions:

Find conditions under which a quantified polynomial formula is true:

Decide the existence of solutions of a univariate polynomial equation:

Decide the existence of solutions of a univariate polynomial inequality:

Decide the existence of solutions of a multivariate polynomial system:

Decide the truth value of fully quantified polynomial formulas:

Decide the existence of solutions of an exp-log equation:

Decide the existence of solutions of an exp-log inequality:

Decide the existence of solutions of an elementary function equation in a bounded interval:

Decide the existence of solutions of a holomorphic function equation in a bounded interval:

Decide the existence of solutions of a periodic elementary function equation:

Fully quantified formulas exp-log in the first variable and polynomial in the other variables:

Fully quantified formulas elementary and bounded in the first variable:

Fully quantified formulas holomorphic and bounded in the first variable:

Find conditions under which a linear system has solutions:

Find conditions under which a quadratic system has solutions:

Find conditions under which a polynomial system has solutions:

Find conditions under which a formula linear in quantified variables is true:

Find conditions under which a formula quadratic in quantified variables is true:

Find conditions under which a quantified polynomial formula is true:

Decide the existence of solutions of a linear system of equations:

Decide the existence of solutions of a linear system of equations and inequalities:

Decide the existence of solutions of a univariate polynomial equation:

Decide the existence of solutions of a univariate polynomial inequality:

Decide the existence of solutions of Frobenius equations:

Decide the existence of solutions of binary quadratic equations:

Decide the existence of solutions of a Thue equation:

Decide the existence of solutions of a sum of squares equation:

Decide the existence of solutions of a bounded system of equations and inequalities:

Decide the existence of solutions of a system of congruences:

Decide the satisfiability of a Boolean formula:

Find conditions under which a quantified Boolean formula is true:

Decide the existence of solutions of an equation involving a real and a complex variable:

Decide the existence of solutions of an inequality involving Abs[x]:

Find under what conditions a fourth power of a complex number is real:

Options (4)

Here the solutions for x are expressed in terms of y:

With

True, Resolve gives explicit numeric values for x:

By default Resolve does not use general formulas for solving cubics in radicals:

With Cubics->True, Resolve expresses roots of cubics in terms of radicals:

By default Resolve does not use general formulas for solving quartics in radicals:

With Quartics->True, Resolve expresses roots of quartics in terms of radicals:

This computation takes a long time due to high degrees of algebraic numbers involved:

With WorkingPrecision

you get an answer faster, but it may be incorrect:

Applications (6)

Find conditions for a quintic to have all roots equal:

Prove the inequality between the arithmetic mean and the geometric mean:

Prove a special case of Hölder's inequality:

Prove a special case of Minkowski's inequality:

Find conditions for a quadratic to be always positive:

Test whether one region is included in another:

Plot the relationship:

Properties & Relations (3)

For fully quantified systems of equations and inequalities, Resolve is equivalent to Reduce:

A solution instance can be found with FindInstance:

For systems with free variables, Resolve may return an unsolved system:

Reduce eliminates quantifiers and solves the resulting system:

Eliminate can be used to eliminate variables from systems of complex polynomial equations:

Resolve gives the same equations, but may also give inequations:

Possible Issues (1)

Because x appears in an inequality, it is assumed to be real:

This allows complex values of x for which both sides of the inequality are real: