摘要
不等式的机器判定,因其广泛的用途和内在的复杂性,已成为定理自动证明领域的研究热点和难点.针对代数不等式提出了一种分拆降幂的机械化判定方法.首先对待证的n元不等式进行齐次化对称化处理,再通过初等对称式表示和降幂分拆,将其等价转化为具有特殊形式的一类多项式不等式,然后对多项式的系数作非负性判定.当转化后的多项式非平凡即系数不是全为非负时,则可以应用经改进的柱形分解程序BOTTEMA和QEPCAD对其作整体判定,或利用多项式完全判别系统,将其转化为一组n-2变元不等式的判定问题再进行判定.最后将此方法编制为Maple通用程序SymProve3,能够快速判定大量次数高至数百、项数数千的多元代数不等式,形成了一个以降低幂次数为主要证题特征的代数不等式判定系统.将其应用于《567 Nice and Hard Inequalities》中列出的209个多元初等不等式的证明,仅用33秒.
Mechanical inequality proving has been a hot and difficult point in the field of automated theorem proving. In this paper, we provide a mechanical algo- rithm for determining a polynomial inequality to be true or not. Firstly, the original inequality with n variables is processed by homogenizing and symmetrizing, and then equivalently reduced to a class of polynomial inequalities in a special form with symmetric decomposition and degree-decreasing method. If all coefficients are positive, then it means the inequality has been proved. Otherwise, it can be proven by the tools of cylindrical algebraic decomposition, such as QEPCAD and BOTTEMA, or be transferred into a set of polynomial inequalities only with n - 2 variables by making use of complete discrimination system implemented into a Maple program named for polynomials. This approach has been SymProve3, and can prove many algebraic inequalities with degrees in hundreds or terms in thousands. At last, SymProve3 has been successfully applied to prove 209 elementary multivariate polynomial inequalities from the book 《 567 Nice and Hard Inequalities 》 within only 33 seconds.
出处
《系统科学与数学》
CSCD
北大核心
2013年第2期179-196,共18页
Journal of Systems Science and Mathematical Sciences
基金
上海市自然科学基金(11ZR1411500)
上海市教委科研创新项目(11ZZ37)
上海市重点学科建设项目(B412)
高等学校博士学科点专项科研基金(20110076120015)
国家自然科学基金创新群体项目(61021004)资助课题
关键词
不等式证明
分拆
降幂
多项式完全判别系统
Algebraic inequality proving, decomposition, degree-decreasing, complete discrimination system for polynomials.
