徐 嘉(西南民族大学计算机科学与技术学院，四川 成都 610041)

三类根式不等式的有理化与机器证明

徐 嘉
(西南民族大学计算机科学与技术学院，四川 成都 610041)

摘 要：研究了三类根式不等式的有理化与机器证明.首先给出了三类根式不等式成立的充分必要条件，即等价的有理不等式组.然后介绍了伴随多项式概念，并建立了一个算法SimplexM.SimplexM能够处理带有连结词∧(and)和∨(or)的多项式不等式组.最后给出了大量的应用实例，证实了这一方法的有效性.

关键词：根式不等式；有理化；单纯剖分方法

根式不等式的自动证明是定理机器证明中的热点和难点.通用的方法是使用一些消去手段(如Groebner基，结式等)去除根式，然后转化为相应的实量词公式加以解决.其中值得特别注意的是杨路的降维方法[1，2，3].它的特点是不增加新的变元，保持较低的维数，从而有非常高的运行效率.根据其方法编制的软件Bottema是目前最为常用的不等式证明软件，已为国内外广大不等式研究者所熟悉.但是对于一些比较特殊的根式不等式类，仍然需要更加精细的研究，以进一步提高证明的效率.在文[4]中由本文作者及合作者给出了一类根式不等式的高效算法.它的主要思想是基于”有理化＋差分代换”的证明模式.其中有理化步骤是依赖于如下的结果.

定理(杨路)设u，v，w，t都是非负实数，则不等式

成立的充分必要条件是下列c0，c1，c2，c3都成立

其中σ1= u＋v＋w，σ2= uv＋vw＋wu，σ3= uvw.

上述定理中的c0包含了一类代数数的极小多项式，相关的……