Resolve
Details and Options
 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 statement expr can be any logical combination of:

lhs==rhs equations lhs!=rhs inequations lhs>rhs or lhs>=rhs inequalities expr∈dom domain specifications {x,y,…}∈reg region specification ForAll[x,cond,expr] universal quantifiers Exists[x,cond,expr] existential quantifiers  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.
 Resolve[expr] can in principle always eliminate quantifiers for any Boolean expression expr.
Examples
open allclose allBasic Examples (4)
Scope (52)
Complex Domain (6)
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:
Real Domain (18)
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 explog equation:
Decide the existence of solutions of an explog 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 explog 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:
Integer Domain (10)
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:
Boolean Domain (2)
Finite Field Domains (5)
Mixed Domains (3)
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)
Backsubstitution (1)
Cubics (1)
Quartics (1)
WorkingPrecision (1)
This computation takes a long time due to high degrees of algebraic numbers involved:
With WorkingPrecision>100 you get an answer faster, but it may be incorrect:
Applications (9)
Polynomials (2)
Theorem Proving (3)
Geometry (4)
The region is a subset of , if is true. Show that Disk[{0,0},{2,1}] is a subset of Rectangle[{2,1},{2,1}]:
Show that Cylinder[]⊆Ball[{0,0,0},2]:
A region is disjoint from if . Show that Circle[{0,0},2] and Disk[{0,0},1] are disjoint:
There are no points in the intersection, so they are disjoint:
A region intersects if . Show that Circle[{0,0},1] intersects Disk[{1/2,0},1]:
Properties & Relations (5)
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:
Find a formula description of a TransformedRegion:
Compute a formula description of using RegionMember:
Check that the formulas are equivalent:
Resolve shows that the polynomial is nonnegative:
Use PolynomialSumOfSquaresList to represent as a sum of squares:
The Motzkin polynomial is nonnegative, but is not a sum of squares:
Text
Wolfram Research (2003), Resolve, Wolfram Language function, https://reference.wolfram.com/language/ref/Resolve.html (updated 2023).
CMS
Wolfram Language. 2003. "Resolve." Wolfram Language & System Documentation Center. Wolfram Research. Last Modified 2023. https://reference.wolfram.com/language/ref/Resolve.html.
APA
Wolfram Language. (2003). Resolve. Wolfram Language & System Documentation Center. Retrieved from https://reference.wolfram.com/language/ref/Resolve.html