WOLFRAM

Wolfram Language & System Documentation Center
Wolfram Language Home Page »

Resolve
✖
Resolve

Updated in 14

✖
Resolve[expr]

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

✖
Resolve[expr,dom]

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

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==rhsequations
    lhs!=rhsinequations
    lhs>rhs or lhs>=rhs inequalities
    expr∈domdomain specifications
    {x,y,…}∈regregion 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 all

Basic Examples  (4)Summary of the most common use cases

Prove that the unit disk is nonempty:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-e072jt
Out[1]=1

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-jnjj6b
Out[1]=1

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-fl732j
Out[1]=1

Find the projection of a geometric region:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-3qq5us
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-8wyqkl
Out[2]=2

Scope  (52)Survey of the scope of standard use cases

Complex Domain  (6)

Decide the existence of solutions of a univariate polynomial equation:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-o97tp
Out[1]=1

Decide the existence of solutions of a multivariate polynomial system:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-ftau4n
Out[1]=1

Decide the truth value of fully quantified polynomial formulas:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-g7hwsd
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-bmpaxf
Out[2]=2

Find conditions under which a polynomial equation has solutions:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-drvio4
Out[1]=1

Find conditions under which a polynomial system has solutions:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-nk5j0r
Out[1]=1

Find conditions under which a quantified polynomial formula is true:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-byt21l
Out[1]=1

Real Domain  (18)

Decide the existence of solutions of a univariate polynomial equation:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-gyjz0
Out[1]=1

Decide the existence of solutions of a univariate polynomial inequality:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-fwu95i
Out[1]=1

Decide the existence of solutions of a multivariate polynomial system:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-gr7crv
Out[1]=1

Decide the truth value of fully quantified polynomial formulas:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-brp8ku
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-cpxl1h
Out[2]=2

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-gvp15g
Out[1]=1

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-kyie2
Out[1]=1

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-imjan8
Out[1]=1

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-nl029
Out[1]=1

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-dm2lpf
Out[1]=1

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-e6l4v8
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-b5zzk3
Out[2]=2

Fully quantified formulas elementary and bounded in the first variable:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-8arqe
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-ec9nd2
Out[2]=2

Fully quantified formulas holomorphic and bounded in the first variable:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-epcw0p
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-bkdxj
Out[2]=2

Find conditions under which a linear system has solutions:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-m9jkw
Out[1]=1

Find conditions under which a quadratic system has solutions:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-e17391
Out[1]=1

Find conditions under which a polynomial system has solutions:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-dijh5x
Out[1]=1

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-lfcchk
Out[1]=1

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-c129o7
Out[1]=1

Find conditions under which a quantified polynomial formula is true:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-kdrucq
Out[1]=1

Integer Domain  (10)

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-sz2ju
Out[1]=1

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-fulreq
Out[1]=1

Decide the existence of solutions of a univariate polynomial equation:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-km7sh0
Out[1]=1

Decide the existence of solutions of a univariate polynomial inequality:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-36h74
Out[1]=1

Decide the existence of solutions of Frobenius equations:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-cjs3ts
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-deaki
Out[2]=2

Decide the existence of solutions of binary quadratic equations:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-g1rl8c
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-bk2dj1
Out[2]=2

Decide the existence of solutions of a Thue equation:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-enjls9
Out[1]=1

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-hsrd0b
Out[1]=1

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-jqvrli
Out[1]=1

Decide the existence of solutions of a system of congruences:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-cpi4z8
Out[1]=1

Boolean Domain  (2)

Decide the satisfiability of a Boolean formula:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-hlzjwe
Out[1]=1

Find conditions under which a quantified Boolean formula is true:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-cmod07
Out[1]=1

Finite Field Domains  (5)

Decide the existence of solutions of univariate equations:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-cfndqf
Out[2]=2
In[3]:=3
✖
https://wolfram.com/xid/0bn6rwi-gyftoc
Out[3]=3

Verify that a univariate equation is satisfied by all field elements:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-f6gotk
Out[1]=1

Decide the existence of solutions of systems of linear equations:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-hef9nj
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-dyppb
Out[2]=2

Decide the existence of solutions of systems of polynomial equations:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-fi2b3p
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-fna1o8
Out[2]=2

Eliminate quantifiers:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-c3cw8z
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-ixizko
Out[2]=2

Mixed Domains  (3)

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-gni56x
Out[1]=1

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-gle2zl
Out[1]=1

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-fhjebh
Out[1]=1

Geometric Regions  (8)

Test :

In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-fqngja
In[4]:=4
✖
https://wolfram.com/xid/0bn6rwi-eckgme
Out[4]=4

Get conditions for :

In[6]:=6
✖
https://wolfram.com/xid/0bn6rwi-bwhcrz
In[8]:=8
✖
https://wolfram.com/xid/0bn6rwi-d2bvqv
Out[8]=8

Project a cone to the - plane:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-b9wofb
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-j0un4z
Out[2]=2

Plot it:

In[3]:=3
✖
https://wolfram.com/xid/0bn6rwi-tc2ldk
Out[3]=3

An implicitly defined region:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-vvkhdz
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-b8ttk3
Out[2]=2

A parametrically defined region:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-juwcyb
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-fo5so0
Out[2]=2

Derived regions:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-mi7sv6
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-25kgk
Out[2]=2

Plot it:

In[3]:=3
✖
https://wolfram.com/xid/0bn6rwi-r1kcx
Out[3]=3

Regions dependent on parameters:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-9d869w
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-fuuwc4
Out[2]=2

The conditions on indicate when the line intersects the circle:

In[3]:=3
✖
https://wolfram.com/xid/0bn6rwi-ddvzpv
Out[3]=3

A condition for :

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-k1jnua
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-h8cff
Out[2]=2

The condition tells when :

In[3]:=3
✖
https://wolfram.com/xid/0bn6rwi-cuvibo
Out[3]=3

Vector variables:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-c4gkcy
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-ft2kkm
Out[2]=2

Options  (4)Common values & functionality for each option

Backsubstitution  (1)

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-cou2ej
Out[1]=1

With Backsubstitution->True, Resolve gives explicit numeric values for x:

In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-ghpqxz
Out[2]=2

Cubics  (1)

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-i4zclq
Out[1]=1

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

In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-b30q6t
Out[2]=2

Quartics  (1)

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-j0l7m7
Out[1]=1

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

In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-k4fo5
Out[2]=2

WorkingPrecision  (1)

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-joy4r1
Out[1]=1

With WorkingPrecision->100 you get an answer faster, but it may be incorrect:

In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-kjnccl
Out[2]=2

Applications  (9)Sample problems that can be solved with this function

Polynomials  (2)

Find conditions for a quintic to have all roots equal:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-c4v8pa
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-lrsikb
Out[2]=2

Find conditions for a quadratic to be always positive:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-ch2e7
Out[1]=1

Theorem Proving  (3)

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-d09mxl
Out[1]=1

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-jc94i0
Out[1]=1

Prove a special case of Minkowski's inequality:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-bc5cii
Out[1]=1

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}]:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-18g7a
In[3]:=3
✖
https://wolfram.com/xid/0bn6rwi-c2c6yf
Out[3]=3

Plot it:

In[4]:=4
✖
https://wolfram.com/xid/0bn6rwi-dplxmk
Out[4]=4

Show that Cylinder[]⊆Ball[{0,0,0},2]:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-bthjls
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-ba7xve
Out[2]=2

Plot it:

In[3]:=3
✖
https://wolfram.com/xid/0bn6rwi-fn0f55
Out[3]=3

A region is disjoint from if . Show that Circle[{0,0},2] and Disk[{0,0},1] are disjoint:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-iczok

There are no points in the intersection, so they are disjoint:

In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-h6331u
Out[2]=2

Plot it:

In[3]:=3
✖
https://wolfram.com/xid/0bn6rwi-ei5vty
Out[3]=3

A region intersects if . Show that Circle[{0,0},1] intersects Disk[{1/2,0},1]:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-j5q9j

There are points in the intersection:

In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-ekg231
Out[2]=2

Plot it:

In[3]:=3
✖
https://wolfram.com/xid/0bn6rwi-rvbro
Out[3]=3

Properties & Relations  (5)Properties of the function, and connections to other functions

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-nl87yt
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-f9nyzh
Out[2]=2

A solution instance can be found with FindInstance:

In[3]:=3
✖
https://wolfram.com/xid/0bn6rwi-bb52em
Out[3]=3

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-et9t7m
Out[1]=1

Reduce eliminates quantifiers and solves the resulting system:

In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-dfsd54
Out[2]=2

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-gqu0wc
Out[1]=1

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

In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-jni7vp
Out[2]=2

Find a formula description of a TransformedRegion:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-mxt4j
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-gwbfi2
Out[2]=2

Compute a formula description of using RegionMember:

In[3]:=3
✖
https://wolfram.com/xid/0bn6rwi-ddt44r
Out[3]=3

Check that the formulas are equivalent:

In[4]:=4
✖
https://wolfram.com/xid/0bn6rwi-mou1qy
Out[4]=4

Resolve shows that the polynomial is non-negative:

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-b2qs46
In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-cqgp6y
Out[2]=2

Use PolynomialSumOfSquaresList to represent as a sum of squares:

In[3]:=3
✖
https://wolfram.com/xid/0bn6rwi-gucy7i
Out[3]=3
In[4]:=4
✖
https://wolfram.com/xid/0bn6rwi-bmrxo2
Out[4]=4

The Motzkin polynomial is non-negative, but is not a sum of squares:

In[5]:=5
✖
https://wolfram.com/xid/0bn6rwi-ltua3e
In[6]:=6
✖
https://wolfram.com/xid/0bn6rwi-qm557
Out[6]=6
In[7]:=7
✖
https://wolfram.com/xid/0bn6rwi-2zhfo
Out[7]=7

Possible Issues  (1)Common pitfalls and unexpected behavior

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

In[1]:=1
✖
https://wolfram.com/xid/0bn6rwi-kyiih
Out[1]=1

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

In[2]:=2
✖
https://wolfram.com/xid/0bn6rwi-b58xns
Out[2]=2
Wolfram Research (2003), Resolve, Wolfram Language function, https://reference.wolfram.com/language/ref/Resolve.html (updated 2024).
✖
Wolfram Research (2003), Resolve, Wolfram Language function, https://reference.wolfram.com/language/ref/Resolve.html (updated 2024).

Text

Wolfram Research (2003), Resolve, Wolfram Language function, https://reference.wolfram.com/language/ref/Resolve.html (updated 2024).

✖
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.

✖
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

✖
Wolfram Language. (2003). Resolve. Wolfram Language & System Documentation Center. Retrieved from https://reference.wolfram.com/language/ref/Resolve.html

BibTeX

@misc{reference.wolfram_2025_resolve, author="Wolfram Research", title="{Resolve}", year="2024", howpublished="\url{https://reference.wolfram.com/language/ref/Resolve.html}", note=[Accessed: 19-June-2025 ]}

✖
@misc{reference.wolfram_2025_resolve, author="Wolfram Research", title="{Resolve}", year="2024", howpublished="\url{https://reference.wolfram.com/language/ref/Resolve.html}", note=[Accessed: 19-June-2025 ]}

BibLaTeX

@online{reference.wolfram_2025_resolve, organization={Wolfram Research}, title={Resolve}, year={2024}, url={https://reference.wolfram.com/language/ref/Resolve.html}, note=[Accessed: 19-June-2025 ]}

✖
@online{reference.wolfram_2025_resolve, organization={Wolfram Research}, title={Resolve}, year={2024}, url={https://reference.wolfram.com/language/ref/Resolve.html}, note=[Accessed: 19-June-2025 ]}