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 all close allBasic Examples (4)
Prove that the unit disk is nonempty:
Resolve[Exists[{x, y}, x ^ 2 + y ^ 2 < 1]]Find the conditions for a quadratic form over the reals to be positive:
Resolve[ForAll[x, ax ^ 2 + bx + c > 0], Reals]Find conditions for a quadratic to have at least two distinct complex roots:
Resolve[Exists[{x, y}, a x ^ 2 + b x + c == 0 && a y ^ 2 + b y + c == 0 && x ≠ y]]Find the projection of a geometric region:
Resolve[Exists[z, {x, y, z}∈Cylinder[{{0, 0, 0}, {1, 1, 1}}, 2]], Reals]RegionPlot[%, {x, -2, 3}, {y, -2, 3}]Scope (52)
Complex Domain (6)
Decide the existence of solutions of a univariate polynomial equation:
Resolve[Exists[x, x ^ 7 + 3 x - 11 == 0]]Decide the existence of solutions of a multivariate polynomial system:
Resolve[Exists[{x, y}, x ^ 2 + y ^ 2 == 1 && x ^ 3 - y ^ 2 == 2 && x y ≠ 3]]Decide the truth value of fully quantified polynomial formulas:
Resolve[ForAll[{a, b, c}, Exists[x, a x ^ 2 + b x + c == 0]]]Resolve[ForAll[{b, c}, Exists[x, x ^ 2 + b x + c == 0]]]Find conditions under which a polynomial equation has solutions:
Resolve[Exists[x, (a ^ 2 - b ^ 3 + 1)x ^ 7 + (a ^ 2 - a b + 1) x ^ 2 - 3 == 0]]Find conditions under which a polynomial system has solutions:
Resolve[Exists[{x, y}, a x ^ 2 + b y ^ 2 == 1 && b x - a y == 2 && x ≠ y]]Find conditions under which a quantified polynomial formula is true:
Resolve[ForAll[c, Exists[x, a x ^ 2 + b x + c == 0]]]Real Domain (18)
Decide the existence of solutions of a univariate polynomial equation:
Resolve[Exists[x, x ^ 7 + 3 x - 11 == 0], Reals]Decide the existence of solutions of a univariate polynomial inequality:
Resolve[Exists[x, x ^ 4 + 3 x + 11 ≤ 0], Reals]Decide the existence of solutions of a multivariate polynomial system:
Resolve[Exists[{x, y}, x ^ 2 + y ^ 2 ≤ 11 && x ^ 3 - y ^ 2 == 2 && x y > 3], Reals]Decide the truth value of fully quantified polynomial formulas:
Resolve[ForAll[{a, b, c}, Exists[x, a x ^ 2 + b x + c ≥ 0]], Reals]Resolve[ForAll[{b, c}, Exists[x, x ^ 2 + b x + c ≥ 0]], Reals]Decide the existence of solutions of an exp-log equation:
Resolve[Exists[x, Exp[x] - 2x Log[x] + 3x ^ x == 4], Reals]Decide the existence of solutions of an exp-log inequality:
Resolve[Exists[x, x ^ Sqrt[Pi] - 2Log[1 / (x ^ 2 + 1)] + E ^ x < 1], Reals]Decide the existence of solutions of an elementary function equation in a bounded interval:
Resolve[Exists[x, -1 < x < 1, Sin[Sin[Sin[x]]] - x == 1 / 7], Reals]Decide the existence of solutions of a holomorphic function equation in a bounded interval:
Resolve[Exists[x, 1 < x < 2, Gamma[x] - BesselJ[2, x] == x + 1], Reals]
Decide the existence of solutions of a periodic elementary function equation:
Resolve[Exists[x, Exp[Sin[x]] - Sin[3 Cos[x]] == Tan[x]], Reals]Fully quantified formulas exp-log in the first variable and polynomial in the other variables:
Resolve[Exists[x, ForAll[y, E ^ x y ^ 3 + Log[x]y == 1 && x y + E ^ x / x ≥ 2]], Reals]Resolve[Exists[{x, y}, y ^ 2 E ^ E ^ x - y E ^ x - x == 1], Reals]Fully quantified formulas elementary and bounded in the first variable:
Resolve[ForAll[x, -1 < x < 0, Exists[y, Sin[x - Cos[x]] y ^ 3 - x == 1]], Reals]Resolve[Exists[{x, y}, Sin[x - Exp[x]] y ^ 3 - x == 2 && x ^ 2 + y ^ 2 ≤ 1], Reals]Fully quantified formulas holomorphic and bounded in the first variable:
Resolve[ForAll[x, -1 < x < 1, Exists[y, y ^ 3 - BesselJ[2, x + 2] y - y - 3 x == -2]], Reals]Resolve[Exists[{x, y}, 1 < x < 2 && Gamma[x] y ^ 2 - x == -5], Reals]Find conditions under which a linear system has solutions:
Resolve[Exists[{x, y}, a x + b y ≥ 1 && (a ^ 2 - b)x - (a - b ^ 2)y == 2], Reals]Find conditions under which a quadratic system has solutions:
Resolve[Exists[x, a x ^ 2 + b x + c ≥ 0 && c x ^ 2 + a ^ 3 - b ^ 3 == 2], Reals]Find conditions under which a polynomial system has solutions:
Resolve[Exists[{x, y}, a x ^ 4 + b y ^ 4 == 1 && x - a y ^ 3 ≥ 2], Reals]Find conditions under which a formula linear in quantified variables is true:
Resolve[ForAll[c, Exists[{x, y}, a x + b y + c == 0 && c x + a y ≥ b]], Reals]Find conditions under which a formula quadratic in quantified variables is true:
Resolve[ForAll[c, c ^ 2 < a ^ 2 - b ^ 3, Exists[x, a x ^ 2 + b x + c == 0]], Reals]Find conditions under which a quantified polynomial formula is true:
Resolve[ForAll[y, Exists[x, (a ^ 2 - 1)x y - (2 a - 1) y ^ 4 + a ^ 3 ≥ 2]], Reals]Integer Domain (10)
Decide the existence of solutions of a linear system of equations:
Resolve[Exists[{x, y, z}, 2 x + 3y - 5z == 1 && 3x - 4y + 7z == 3], Integers]Decide the existence of solutions of a linear system of equations and inequalities:
Resolve[Exists[{x, y, z}, 2 x + 3y == 4 && 3x - 4y ≤ 5 && x - 2y > -21], Integers]Decide the existence of solutions of a univariate polynomial equation:
Resolve[Exists[x, x ^ 1000 - 2x ^ 777 + 1 == 0], Integers]Decide the existence of solutions of a univariate polynomial inequality:
Resolve[Exists[x, x ^ 5 - 2x + 1 < 0], Integers]Decide the existence of solutions of Frobenius equations:
Resolve[Exists[{x, y, z, t}, 1221x + 3434y + 5566z + 8778t == 90909 && x ≥ 0 && y ≥ 0 && z ≥ 0 && t ≥ 0], Integers]Resolve[Exists[{x, y, z, t}, 1221x + 3434y + 5566z + 8778t == 909090 && x ≥ 0 && y ≥ 0 && z ≥ 0 && t ≥ 0], Integers]Decide the existence of solutions of binary quadratic equations:
Resolve[Exists[{x, y}, x ^ 2 + x y + y ^ 2 == 107], Integers]Resolve[Exists[{x, y}, x ^ 2 - 3y ^ 2 == 22 && x > 0 && y > 0], Integers]Decide the existence of solutions of a Thue equation:
Resolve[Exists[{x, y}, x ^ 3 - 2x ^ 2 y + y ^ 3 == 2], Integers]Decide the existence of solutions of a sum of squares equation:
Resolve[Exists[{x, y, z, t}, x ^ 2 + 4y ^ 2 + 9z ^ 2 + 16t ^ 2 == 354], Integers]Decide the existence of solutions of a bounded system of equations and inequalities:
Resolve[Exists[{x, y, z}, x ^ 4 + y ^ 4 + z ^ 4 ≤ 500 && x + y ^ 2 + z ^ 3 == 32], Integers]Decide the existence of solutions of a system of congruences:
Resolve[Exists[{x, y}, Mod[x ^ 2 + y ^ 2, 2] == 1 && Mod[x - 2y, 3] == 2], Integers]Boolean Domain (2)
Decide the satisfiability of a Boolean formula:
Resolve[Exists[{a, b, c, d}, Xor[a, b, c, d] && (a || b) && (c || d)], Booleans]Find conditions under which a quantified Boolean formula is true:
Resolve[Exists[a, ForAll[b, Nand[a, b, c, d] && (a || b) && (c || d)]], Booleans]Finite Field Domains (5)
Decide the existence of solutions of univariate equations:
ℱ = FiniteField[53, 4];
Resolve[Exists[x, x ^ 5 + ℱ[123]x == ℱ[234]]]Resolve[Exists[x, x ^ 9 + 2 x + 3 == 0], ℱ]Verify that a univariate equation is satisfied by all field elements:
ℱ = FiniteField[3, 2];
Resolve[ForAll[x, x ^ 8 == x], ℱ]Decide the existence of solutions of systems of linear equations:
ℱ = FiniteField[71, 2];
Resolve[Exists[{x, y}, ℱ[123]x + ℱ[234]y == ℱ[345] && ℱ[321]x + ℱ[432]y == ℱ[543]]]Resolve[Exists[{x, y, z}, ℱ[1234]x + ℱ[2345]y + ℱ[3456]z == ℱ[4567] && ℱ[1]x + ℱ[2]y + ℱ[3]z == ℱ[4] && ℱ[2471]x + ℱ[4696]y + ℱ[1809]z == ℱ[123]]]Decide the existence of solutions of systems of polynomial equations:
ℱ = FiniteField[7, 5];
Resolve[Exists[{x, y, z}, x ^ 2 + y ^ 2 + z ^ 2 == 21], ℱ]Resolve[Exists[{x, y, z}, ℱ[321]x ^ 3 + ℱ[432]y ^ 3 + ℱ[543]z ^ 3 == ℱ[654] && x ^ 2 == ℱ[333]y z + ℱ[111]]]ℱ = FiniteField[2, 5];
Resolve[Exists[z, ℱ[1]x + ℱ[3]y + ℱ[5]z == ℱ[7] && ℱ[21]x + ℱ[23]y + ℱ[25]z == ℱ[27]]]Resolve[Exists[{y, z}, ℱ[1]x ^ 2 + ℱ[2]y ^ 3 + ℱ[3]z ^ 4 == ℱ[4] && ℱ[5]x ^ 4 + ℱ[6]y ^ 3 + ℱ[7]z ^ 2 == ℱ[8] && x y z != ℱ[0]]]Mixed Domains (3)
Decide the existence of solutions of an equation involving a real and a complex variable:
Resolve[Exists[{x, y}, Element[x, Reals], x ^ 2 + y ^ 2 == -1]]Decide the existence of solutions of an inequality involving Abs[x]:
Resolve[Exists[x, Abs[x] ^ 2 - 3Abs[x] < 1]]Find under what conditions a fourth power of a complex number is real:
Resolve[Exists[x, Element[x, Reals], y ^ 4 == x]]Geometric Regions (8)
Subscript[ℛ, 1] = Rectangle[];
Subscript[ℛ, 2] = Disk[{0, 0}, 2];Resolve[Subscript[∀, {x, y}, {x, y}∈Subscript[ℛ, 1]]{x, y}∈Subscript[ℛ, 2], Reals]
Subscript[ℛ, 1] = Rectangle[];
Subscript[ℛ, 2] = Disk[{0, 0}, r];Resolve[Subscript[∀, {x, y}, {x, y}∈Subscript[ℛ, 1]]{x, y}∈Subscript[ℛ, 2], Reals]Project a cone to the 
-
plane:
ℛ = Cone[{{3, 2, 1}, {1, 2, 3}}, 1];Resolve[Exists[z, {x, y, z}∈ℛ], Reals]RegionPlot[%, {x, 0, 4}, {y, 0, 4}]ℛ = ImplicitRegion[a + 2 b - 3 c ≥ 1 && a b c == 7, {a, b, c}];Resolve[Subscript[∃, z, {x, y, z}∈ℛ]x^2 + y z == 1, Reals]A parametrically defined region:
ℛ = ParametricRegion[{s^2, t^2, s t}, {s, t}];Resolve[Subscript[∃, {y, z}](x^2 + y^2 + z^2 == 1 && {x, y, z}∈ℛ), Reals]ℛ = RegionIntersection[Ball[{0, 0, 0}, 2], Ball[{1, 1, 1}, 2]];Resolve[Subscript[∃, z]{x, y, z}∈ℛ, Reals]RegionPlot[%, {x, -2, 3}, {y, -2, 3}]Regions dependent on parameters:
Subscript[ℛ, 1] = InfiniteLine[{{2, 0}, {0, t}}];
Subscript[ℛ, 2] = Circle[];Resolve[Subscript[∃, {x, y}, {x, y}∈Subscript[ℛ, 1]]{x, y}∈Subscript[ℛ, 2], Reals]The conditions on 
indicate when the line intersects the circle:
Graphics[{Table[{If[%, Green, Red], Subscript[ℛ, 1]}, {t, -2, 2, 0.5}], {Blue, Subscript[ℛ, 2]}}]
Subscript[ℛ, 1] = Disk[{a, b}];
Subscript[ℛ, 2] = Triangle[{{0, 0}, {0, 5}, {7, 0}}];Resolve[Subscript[∀, {x, y}, {x, y}∈Subscript[ℛ, 1]]{x, y}∈Subscript[ℛ, 2], Reals]
Graphics[{{Blue, Subscript[ℛ, 2]}, Table[If[%, {Opacity[0.8], Green, Subscript[ℛ, 1]}, {Opacity[0.2], Red, Subscript[ℛ, 1]}], {a, 0, 6}, {b, 0, 4}]}]Subscript[ℛ, 1] = Sphere[];
Subscript[ℛ, 2] = InfinitePlane[{{1, 0, 0}, {0, 1, 0}, {0, 0, 1}}];Resolve[Subscript[∃, x, x∈Subscript[ℛ, 1]](y∈Subscript[ℛ, 2] && x.y == 1), Reals]Options (5)
Backsubstitution (1)
Here the solutions for x are expressed in terms of y:
Resolve[Exists[z, x y + z ^ 4 - z == 1 && x ^ 2 + y ^ 2 + z ^ 3 == 10 && a(x ^ 2 - x y + y) ^ 2 ≤ 0 && a > 0], Reals]With Backsubstitution->True, Resolve gives explicit numeric values for x:
Resolve[Exists[z, x y + z ^ 4 - z == 1 && x ^ 2 + y ^ 2 + z ^ 3 == 10 && a(x ^ 2 - x y + y) ^ 2 ≤ 0 && a > 0], Reals, Backsubstitution -> True]Cubics (1)
By default, Resolve does not use general formulas for solving cubics in radicals:
Resolve[Exists[x, x > a && x ^ 3 + x + 1 == 0], Reals]With Cubics->True, Resolve expresses roots of cubics in terms of radicals:
Resolve[Exists[x, x > a && x ^ 3 + x + 1 == 0], Reals, Cubics -> True]Method (1)
This locally sets system options in "InequalitySolvingOptions" and "ReduceOptions" groups:
Resolve[Subscript[∃, x](a x^2 + b x + c) (c x^2 + b x + a) <= 0, Reals, Method -> {"QuadraticQE" -> False}]//AbsoluteTimingBy default Resolve uses the quadratic case of virtual substitution algorithm here:
Resolve[Subscript[∃, x](a x^2 + b x + c) (c x^2 + b x + a) <= 0, Reals]//AbsoluteTimingQuartics (1)
By default, Resolve does not use general formulas for solving quartics in radicals:
Resolve[Exists[x, x > a && x ^ 4 + x - 9 == 0], Reals]With Quartics->True, Resolve expresses roots of quartics in terms of radicals:
Resolve[Exists[x, x > a && x ^ 4 + x - 9 == 0], Reals, Quartics -> True]WorkingPrecision (1)
This computation takes a long time due to high degrees of algebraic numbers involved:
Resolve[Exists[{x, y, z}, x ^ 8 + 2y ^ 8 + 3z ^ 8 ≤ 1 && x ^ 3 - 9y ^ 3 + 7z ^ 3 - x y z ≥ 10], Reals]//TimingWith WorkingPrecision->100 you get an answer faster, but it may be incorrect:
Resolve[Exists[{x, y, z}, x ^ 8 + 2y ^ 8 + 3z ^ 8 ≤ 1 && x ^ 3 - 9y ^ 3 + 7z ^ 3 ≥ 10], Reals, WorkingPrecision -> 100]//TimingApplications (9)
Polynomials (2)
Find conditions for a quintic to have all roots equal:
f[x_] := x ^ 5 + a x ^ 4 + b x ^ 3 + c x ^ 2 + d x + eResolve[Exists[x, f[x] == 0, ForAll[y, f[y] == 0, x == y]]]Find conditions for a quadratic to be always positive:
Resolve[ForAll[x, a x ^ 2 + b x + c > 0], Reals]Theorem Proving (3)
Prove the inequality between the arithmetic mean and the geometric mean:
Resolve[ForAll[{a, b}, a > 0 && b > 0, (a + b) / 2 ≥ Sqrt[a b]], Reals]Prove a special case of Hölder's inequality:
Resolve[ForAll[{a, b, c, d}, a > 0 && b > 0 && c > 0 && d > 0, a c + b d ≤ Sqrt[a ^ 2 + b ^ 2]Sqrt[c ^ 2 + d ^ 2]], Reals]Prove a special case of Minkowski's inequality:
Resolve[ForAll[{a, b, c, d}, Sqrt[(a + c) ^ 2 + (b + d) ^ 2] ≤ Sqrt[a ^ 2 + b ^ 2] + Sqrt[c ^ 2 + d ^ 2]], Reals]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}]:
ℛ = Disk[{0, 0}, {2, 1}];
𝒮 = Rectangle[{-2, -1}, {2, 1}];Resolve[Subscript[∀, {x, y}]{x, y}∈ℛ{x, y}∈𝒮, Reals]Graphics[{{StandardBlue, EdgeForm[Thick], 𝒮}, {StandardYellow, EdgeForm[Thick], ℛ}}]Show that Cylinder[]⊆Ball[{0,0,0},2]:
ℛ = Cylinder[];
𝒮 = Ball[{0, 0, 0}, 2];Resolve[Subscript[∀, {x, y, z}]{x, y, z}∈ℛ{x, y, z}∈𝒮, Reals]Graphics3D[{{Opacity[0.3], 𝒮}, {LightBlue, EdgeForm[Gray], ℛ}}]A region 
is disjoint from 
if 
. Show that Circle[{0,0},2] and Disk[{0,0},1] are disjoint:
ℛ = Circle[{0, 0}, 2];
𝒮 = Disk[{0, 0}, 1];There are no points in the intersection, so they are disjoint:
With[{p = {x, y}}, Resolve[Subscript[∃, p](p∈ℛ∧p∈𝒮), Reals]]Graphics[{{StandardBlue, EdgeForm[Thick], 𝒮}, {Thick, ℛ}}]A region 
intersects 
if 
. Show that Circle[{0,0},1] intersects Disk[{1/2,0},1]:
ℛ = Circle[{0, 0}, 1];
𝒮 = Disk[{1 / 2, 0}, 1];There are points in the intersection:
With[{p = {x, y}}, Resolve[Subscript[∃, p](p∈ℛ∧p∈𝒮), Reals]]Graphics[{{StandardBlue, EdgeForm[Thick], 𝒮}, {Thick, ℛ}}]Properties & Relations (5)
For fully quantified systems of equations and inequalities, Resolve is equivalent to Reduce:
Resolve[Exists[{x, y}, x ^ 2 + y ^ 2 ≤ 3 && x ^ 3 - y ^ 2 == 1]]Reduce[Exists[{x, y}, x ^ 2 + y ^ 2 ≤ 3 && x ^ 3 - y ^ 2 == 1]]A solution instance can be found with FindInstance:
FindInstance[x ^ 2 + y ^ 2 ≤ 3 && x ^ 3 - y ^ 2 == 1, {x, y}]For systems with free variables, Resolve may return an unsolved system:
Resolve[Exists[x, x ^ 2 - 2a x + b < 0 && 2x > a + b ^ 2 - 1], Reals]Reduce eliminates quantifiers and solves the resulting system:
Reduce[Exists[x, x ^ 2 - 2a x + b < 0 && 2x > a + b ^ 2 - 1], {a, b}, Reals]Eliminate can be used to eliminate variables from systems of complex polynomial equations:
eqns = x z == y && x ^ 2 + x ^ 2z ^ 2 == 1;
Eliminate[eqns, z]Resolve gives the same equations, but may also give inequations:
Resolve[Exists[z, eqns]]Find a formula description of a TransformedRegion:
f = Evaluate[{Indexed[#, 1] Indexed[#, 2], Indexed[#, 1] + Indexed[#, 2]}]&;
Subscript[ℛ, 1] = Disk[{0, 0}];
Subscript[ℛ, 2] = TransformedRegion[Subscript[ℛ, 1], f]Subscript[c, 1] = Resolve[Exists[{u, v}, {u, v}∈Subscript[ℛ, 1], And@@Thread[{x, y} == f[{u, v}]]], Reals]Compute a formula description of 
using RegionMember:
Subscript[c, 2] = RegionMember[Subscript[ℛ, 2], {x, y}]Check that the formulas are equivalent:
Resolve[Subscript[∀, {x, y}](Subscript[c, 1]⧦Subscript[c, 2]), Reals]Resolve shows that the polynomial 
is non-negative:
f = x ^ 2 + 2y ^ 2 + 3 z ^ 2 - x y - x z - y z;Resolve[ForAll[{x, y, z}, f >= 0], Reals]Use PolynomialSumOfSquaresList to represent 
as a sum of squares:
PolynomialSumOfSquaresList[f, {x, y, z}]f - %.%//ExpandThe Motzkin polynomial is non-negative, but is not a sum of squares:
m = x ^ 4 y ^ 2 + x ^ 2 y ^ 4 - 3 x ^ 2 y ^ 2 + 1;Resolve[ForAll[{x, y}, m >= 0], Reals]PolynomialSumOfSquaresList[m, {x, y}]
Text
Wolfram Research (2003), Resolve, Wolfram Language function, https://reference.wolfram.com/language/ref/Resolve.html (updated 2024).
CMS
Wolfram Language. 2003. "Resolve." Wolfram Language & System Documentation Center. Wolfram Research. Last Modified 2024. 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