对称型的降幂分拆方法与代数不等式的一个判定系统

作者：陈胜利; 陈良育

来源：系统科学与数学, 2013, (02): 179-196.

• 不等式证明
• 分拆
• 降幂
• 多项式完全判别系统 Algebraic inequality proving
• decomposition
• degree-decreasing
• complete discrimination system for polynomials

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

• 出版日期2013
• 单位华东师范大学