MATHEMATICA 内置符号

Resolve

Resolve[expr]
尝试把 expr 变成一种消除 ForAll 和 Exists 量词的形式.

Resolve

作用于域 dom. dom 常见的选择是 Complexes， Reals 和 Booleans.

更多信息

Resolve 实际上是自动地被 Reduce 应用.

expr 可以包含方程式，不等式，域的设定和量词，和在 Reduce 中形式一样.

Resolve[expr] 的结果总是描述和 expr 完全一样的数学问题，但没有量词.

默认下，Resolve[expr] 假定以代数形式出现在不等式中量是实数，而所有其他的量是复数.

当一个量词如 ForAll 被消去后，其结果将不提及局部变量 x.

如果 expr 仅包含实数或复数域上的多项式方程和不等式，则 Resolve[expr] 原则上总可以消除量词.

对于任何布尔表达式，Resolve[expr] 原则上总可以消除量词.

范例

关闭所有单元

例 (1)

证明单位圆盘非空：

找出二次方形在实数上为正数的条件：

找出二次方程式至少有两个不同的复数根的条件：

证明单位圆盘非空：

In[1]:=

Out[1]=

找出二次方形在实数上为正数的条件：

In[2]:=

Out[2]=

找出二次方程式至少有两个不同的复数根的条件：

In[3]:=

Out[3]=

范围 (39)

决定单一个变量多项式方程解的存在性：

决定一个多元多项式系统解的存在性：

决定完全量化多项式公式的真值：

找出一个多项式方程有解的条件：

找出一个多项式系统有解的条件：

找出一个量化多项式公式为真的条件：

决定一个单变量多项式方程解的存在性：

决定一个单变量多项式不等式解的存在性：

决定一个多元多项式系统解的存在性：

决定完全量化的多项式公式的真值：

决定一个指数-对数方程解的存在性：

决定一个指数-对数不等式解的存在性：

决定一个初等函数方程在有界区间内解的存在性：

决定一个全纯函数方程在有界区间内解的存在性：

决定一个周期初等函数方程解的存在性：

对第一个变量是指数-对数函数，其他变量是多项式的完全量化的公式：

对第一变量为初等函数且有界的完全量化公式：

对第一变量为全纯函数且有界的完全量化的公式：

找到线性系统有解的条件：

找到一个二次系统有解的条件：

找到一个多项式系统有解的条件：

找到一个对量化的变量线性的公式为真的条件：

找到一个对量化的变量为二次形的公式为真的条件：

找到一个量化的多项式公式为真的条件：

决定一个线性方程组解的存在性：

决定一个线性方程和不等式系统解的存在性：

决定一个单变量多项式方程解的存在性：

决定一个单变量多项式不等式解的存在性：

决定Frobenius方程解的存在性：

决定二元二次方程解的存在性：

决定Thue方程解的存在性：

决定一个平方和方程解的存在性：

决定一个方程和不等式的有界系统解的存在性：

决定一个同余系统解的存在性：

决定布尔公式是否被满足：

找到一个量化布尔公式为真的：

决定一个含有实变量和复变量的方程解的存在性：

决定一个含有 Abs[x] 的不等式解的存在性：

找到一个复数的四次幂是实数的条件：

选项 (4)

这里， x 的解是以y 的形式表示的：

设置

True 后， Resolve 给出 x 的明确数值值：

默认情况下， Resolve 不使用以根式表示的三次方程通解公式：

设置 Cubics->True 后， Resolve 以根式的形式表示三次方程的根：

默认情况下， Resolve 不使用以根式表示的四次方程通解公式：

设置 Quartics->True 后， Resolve 以根式的形式表示四次方程的根：

由于含有高次代数数，下面的计算需要很长的时间：

设置 WorkingPrecision

，我们更快地得到答案，但它有可能不正确：

应用 (6)

找到一个五次方程所有根都相等的条件：

证明算术平均值和几何平均值之间的不等式：

证明 Hölder 不等式的一个特例：

证明 Minkowski 不等式的一个特例：

找到一个二次式始终为正的条件：

检验一个区域是否已被另一个区域所包含：

绘制关系图：

属性和关系 (3)

对于完全量化的方程和不等式系统， Resolve 和 Reduce 是等价的：

可以用 FindInstance 找到一个解的个利：

对于含有自由变量的系统， Resolve 可能会返回一个未解的系统：

Reduce 则消去量词并求解所得的系统：

Eliminate 可用于消去复数多项式方程系统的变量：

Resolve 给出同样的方程，但也有可能给出不等式：

可能存在的问题 (1)

因为 x 出现在不等式中，所以它被假定为实数：

下面的情形允许 x 取使不等式的两边都是实数得复数值：

参见

Reduce FindInstance Exists ForAll Conjunction Disjunction CylindricalDecomposition

教程

量词

复数多项式系统

更多关于

布尔运算

逻辑和布尔代数

多项式代数

多项式系统