|
"结式方法" 更准确的叫法是“逐次结式方法”,因为要做多次结式。
“逐次结式方法” 是杨路研究员在上世纪 90 年代提出来的,是不等式自动证明软件Bottema 的基本算法之一。核心思想是对多项式 $f$ 和 $f'$ 作结式消去一个变量, 然后重复这一过程,直到消去所有自由变量,获得只含有参数变量的多项式, 它就是参数所要满足的方程(最值的必要条件)。
举个简单的例子如下:令 $f=x^4+y^6+1-tx^3y$ , $x,y$ 是非负实数。求最大的 $t$ 使不等式 $f\geq 0$ 恒成立。
1 对 $f, f'_x$ 作结式消去 $x$.
$\ \ \ res(f, f'_x, x)=(y^6+1)^2(-27t^4y^4+256y^6+256)$
2. 令 (去除重因子)
$\ \ \ g=(y^6+1)(-27t^4y^4+256y^6+256)$
3 对 $g, g'_y$ 作结式消去 $y$.
$\ \ \ res(g, g'_y, y)=t^{48}(27t^6-2048)^2(27t^6+2048)^2$.
如果满足要求的 $t$ 存在,则 $t$ 必须要满足方程
$t(27t^6-2048)(27t^6+2048)=0$.
明显地,$t$ 不可能是 $0$ 或负数,所以 $t$ 只可能是 $27t^6-2048$ 的正实根。
当然,对大多数例子,你只能依靠计算机,手算几乎是不可能的。 |
|