陈胜利,陈良育
不等式的机器判定,因其广泛的用途和内在的复杂性,已成为定理自动证明领域的研究热点和难点.针对代数不等式提出了一种分拆降幂的机械化判定方法.首先对待证的$n$元不等式进行齐次化对称化处理,再通过初等对称式表示和降幂分拆,将其等价转化为具有特殊形式的一类多项式不等式,然后对多项式的系数作非负性判定.当转化后的多项式非平凡即系数不是全为非负时, 则可以应用经改进的柱形分解程序BOTTEMA和QEPCAD 对其作整体判定, 或利用多项式完全判别系统,将其转化为一组$n-2$变元不等式的判定问题再进行判定.最后将此方法编制为Maple通用程序SymProve3,能够快速判定大量次数高至数百、项数数千的多元代数不等式,形成了一个以降低幂次数为主要证题特征的代数不等式判定系统. 将其应用于《567 Nice and Hard Inequalities》 中列出的209个多元初等不等式的证明,仅用33秒.