({{, (RefLink[Resolve, paclet:ref/Resolve])[expr]
attempts to resolve expr into a form that eliminates (RefLink[ForAll, paclet:ref/ForAll]) and (RefLink[Exists, paclet:ref/Exists]) quantifiers. }, {, (RefLink[Resolve, paclet:ref/Resolve])[expr,dom]
works over the domain dom. Common choices of dom are (RefLink[Complexes, paclet:ref/Complexes]), (RefLink[Reals, paclet:ref/Reals]), and (RefLink[Booleans, paclet:ref/Booleans]). }})

OpenersNotesSection(Spacer1)Details and Options

(RefLink[Resolve, paclet:ref/Resolve]) is in effect automatically applied by (RefLink[Reduce, paclet:ref/Reduce]).

expr can contain equations, inequalities, domain specifications, and quantifiers, in the same form as in (RefLink[Reduce, paclet:ref/Reduce]).

The statement expr can be any logical combination of:

The result of (RefLink[Resolve, paclet:ref/Resolve])[expr] always describes exactly the same mathematical set as expr, but without quantifiers.

(RefLink[Resolve, paclet:ref/Resolve])[expr] assumes by default that quantities appearing algebraically in inequalities are real, while all other quantities are complex.

When a quantifier such as (RefLink[ForAll, paclet:ref/ForAll])[x,…] is eliminated, the result will contain no mention of the localized variable x.

(RefLink[Resolve, paclet:ref/Resolve])[expr] can in principle always eliminate quantifiers if expr contains only polynomial equations and inequalities over the reals or complexes.

(RefLink[Resolve, paclet:ref/Resolve])[expr] can in principle always eliminate quantifiers for any Boolean expression expr.

OpenersPrimaryExamplesSection(Spacer1)Examples  (69)

OpenersExampleSection0(Spacer1)Basic 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}]

OpenersExampleSection1(Spacer1)Scope  (47)

OpenersExampleSubsection0(Spacer1)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]]]

OpenersExampleSubsection1(Spacer1)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]

OpenersExampleSubsection2(Spacer1)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]

OpenersExampleSubsection3(Spacer1)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]

OpenersExampleSubsection4(Spacer1)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 (RefLink[Abs, paclet:ref/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]]

OpenersExampleSubsection5(Spacer1)Geometric Regions  (8)

Test (Subscript[ℛ, 1])⊆(Subscript[ℛ, 2]):

(Subscript[ℛ, 1])=Rectangle[];
(Subscript[ℛ, 2])=Disk[{0,0},2];

Resolve[(Subscript[∀, {x,y},{x,y}∈(Subscript[ℛ, 1])]){x,y}∈(Subscript[ℛ, 2]),Reals]

Get conditions for (Subscript[ℛ, 1])⊆(Subscript[ℛ, 2]):

(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 x-y plane:

ℛ=Cone[{{3,2,1},{1,2,3}},1];

Resolve[Exists[z,{x,y,z}∈ℛ],Reals]

Plot it:

RegionPlot[%,{x,0,4},{y,0,4}]

An implicitly defined region:

ℛ=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]

Derived regions:

ℛ=RegionIntersection[Ball[{0,0,0},2],Ball[{1,1,1},2]];

Resolve[(Subscript[∃, z]){x,y,z}∈ℛ,Reals]

Plot it:

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 t indicate when the line intersects the circle:

Graphics[{Table[{If[%,Green,Red],(Subscript[ℛ, 1])},{t,-2,2,0.5}],{Blue,(Subscript[ℛ, 2])}}]

A condition for (Subscript[ℛ, 1])⊆(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]

The condition tells when (Subscript[ℛ, 1])⊆(Subscript[ℛ, 2]):

Graphics[{{Blue,(Subscript[ℛ, 2])},Table[If[%,{Opacity[0.8],Green,(Subscript[ℛ, 1])},{Opacity[0.2],Red,(Subscript[ℛ, 1])}],{a,0,6},{b,0,4}]}]

Vector variables:

(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]

OpenersExampleSection2(Spacer1)Options  (4)

OpenersExampleSubsection6(Spacer1)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^4==10&&(x^2-y+3)^2≤0],Reals]//Timing

With Backsubstitution->(RefLink[True, paclet:ref/True]), (RefLink[Resolve, paclet:ref/Resolve]) gives explicit numeric values for x:

Resolve[Exists[z,x y +z^4-z==1&&x^2+y^2+z^4==10&&(x^2-y+3)^2≤0],Reals,Backsubstitution->True]//Timing

OpenersExampleSubsection7(Spacer1)Cubics  (1)

By default, (RefLink[Resolve, paclet:ref/Resolve]) does not use general formulas for solving cubics in radicals:

Resolve[Exists[x,x>a&&x^3+x+1==0],Reals]

With (RefLink[Cubics, paclet:ref/Cubics])->(RefLink[True, paclet:ref/True]), (RefLink[Resolve, paclet:ref/Resolve]) expresses roots of cubics in terms of radicals:

Resolve[Exists[x,x>a&&x^3+x+1==0],Reals,Cubics->True]

OpenersExampleSubsection8(Spacer1)Quartics  (1)

By default, (RefLink[Resolve, paclet:ref/Resolve]) does not use general formulas for solving quartics in radicals:

Resolve[Exists[x,x>a&&x^4+x-9==0],Reals]

With (RefLink[Quartics, paclet:ref/Quartics])->(RefLink[True, paclet:ref/True]), (RefLink[Resolve, paclet:ref/Resolve]) expresses roots of quartics in terms of radicals:

Resolve[Exists[x,x>a&&x^4+x-9==0],Reals,Quartics->True]

OpenersExampleSubsection9(Spacer1)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]//Timing

With (RefLink[WorkingPrecision, paclet:ref/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]//Timing

OpenersExampleSection3(Spacer1)Applications  (9)

OpenersExampleSubsection10(Spacer1)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 + e

Resolve[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]

OpenersExampleSubsection11(Spacer1)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]

OpenersExampleSubsection12(Spacer1)Geometry  (4)

The region ℛ is a subset of 𝒮, ℛ⊆𝒮 if (Subscript[∀, {x,y,…}]){x,y,…}∈ℛ=>{x,y,…}∈𝒮 is true. Show that (RefLink[Disk, paclet:ref/Disk])[{0,0},{2,1}] is a subset of (RefLink[Rectangle, paclet:ref/Rectangle])[{-2,-1},{2,1}]:

ℛ=Disk[{0,0},{2,1}];
𝒮=Rectangle[{-2,-1},{2,1}];

Resolve[(Subscript[∀, {x,y}]){x,y}∈ℛ\[Implies]{x,y}∈𝒮,Reals]

Plot it:

Graphics[{{LightRed,EdgeForm[Gray],𝒮},{LightBlue,EdgeForm[Gray],ℛ}}]

Show that (RefLink[Cylinder, paclet:ref/Cylinder])[]⊆(RefLink[Ball, paclet:ref/Ball])[{0,0,0},2]:

ℛ=Cylinder[];
𝒮=Ball[{0,0,0},2];

Resolve[(Subscript[∀, {x,y,z}]){x,y,z}∈ℛ\[Implies]{x,y,z}∈𝒮,Reals]

Plot it:

Graphics3D[{{Opacity[0.3],𝒮},{LightBlue,EdgeForm[Gray],ℛ}}]

A region ℛ is disjoint from 𝒮 if ℛ⋂𝒮==∅. Show that (RefLink[Circle, paclet:ref/Circle])[{0,0},2] and (RefLink[Disk, paclet:ref/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]]

Plot it:

Graphics[{{LightBlue,EdgeForm[Gray],𝒮},{ℛ}}]

A region ℛ intersects 𝒮 if ℛ⋂𝒮≠∅. Show that (RefLink[Circle, paclet:ref/Circle])[{0,0},1] intersects (RefLink[Disk, paclet:ref/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]]

Plot it:

Graphics[{{LightBlue,EdgeForm[Gray],𝒮},{ℛ}}]

OpenersExampleSection4(Spacer1)Properties & Relations  (4)

For fully quantified systems of equations and inequalities, (RefLink[Resolve, paclet:ref/Resolve]) is equivalent to (RefLink[Reduce, paclet:ref/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 (RefLink[FindInstance, paclet:ref/FindInstance]):

FindInstance[x^2+y^2≤3&&x^3-y^2==1,{x,y}]

For systems with free variables, (RefLink[Resolve, paclet:ref/Resolve]) may return an unsolved system:

Resolve[Exists[x,x^2-2a x+b<0&&2x>a+b^2-1],Reals]

(RefLink[Reduce, paclet:ref/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]

(RefLink[Eliminate, paclet:ref/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]

(RefLink[Resolve, paclet:ref/Resolve]) gives the same equations, but may also give inequations:

Resolve[Exists[z,eqns]]

Find a formula description of a (RefLink[TransformedRegion, paclet:ref/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 (Subscript[ℛ, 2]) using (RefLink[RegionMember, paclet:ref/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]

OpenersExampleSection5(Spacer1)Possible Issues  (1)

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

Resolve[Exists[x,x^2<-1]]

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

Resolve[Exists[x,x^2<-1],Complexes]

({{DocumentationFooterIconsRelatedFunction.png, ({{See Also}, {(RefLink[Reduce, paclet:ref/Reduce])  ▪  (RefLink[FindInstance, paclet:ref/FindInstance])  ▪  (RefLink[Exists, paclet:ref/Exists])  ▪  (RefLink[ForAll, paclet:ref/ForAll])  ▪  (RefLink[Conjunction, paclet:ref/Conjunction])  ▪  (RefLink[Disjunction, paclet:ref/Disjunction])  ▪  (RefLink[CylindricalDecomposition, paclet:ref/CylindricalDecomposition])}})}})

({{DocumentationFooterIconsRelatedTutorial.png, ({{Tutorials}, {▪(RefLinkPlain[Quantifiers, paclet:tutorial/Quantifiers])}, {▪(RefLinkPlain[Complex Polynomial Systems, paclet:tutorial/ComplexPolynomialSystems])}})}})

({{DocumentationFooterIconsRelatedGuide.png, ({{Related Guides}, {▪(RefLinkPlain[Theorem Proving, paclet:guide/TheoremProving])}, {▪(RefLinkPlain[Polynomial Algebra, paclet:guide/PolynomialAlgebra])}, {▪(RefLinkPlain[Boolean Computation, paclet:guide/BooleanComputation])}, {▪(RefLinkPlain[Polynomial Systems, paclet:guide/PolynomialSystems])}, {▪(RefLinkPlain[Logic & Boolean Algebra, paclet:guide/LogicAndBooleanAlgebra])}, {▪(RefLinkPlain[Solvers over Regions, paclet:guide/GeometricSolvers])}, {▪(RefLinkPlain[Operations on Sets, paclet:guide/OperationsOnSets])}})}})

({{(Spacer1), ({{(Spacer1)Related Links}, {(Spacer1)▪(RefLinkPlain[(Spacer1)Implementation notes: Algebra and Calculus, paclet:tutorial/SomeNotesOnInternalImplementation#5786])}})}})