系统科学与数学
繫統科學與數學
계통과학여수학
JOURNAL OF SYSTEMS SCIENCE AND MATHEMATICAL SCIENCES
2013年
2期
179-196
,共18页
不等式证明%分拆%降幂%多项式完全判别系统
不等式證明%分拆%降冪%多項式完全判彆繫統
불등식증명%분탁%강멱%다항식완전판별계통
不等式的机器判定,因其广泛的用途和内在的复杂性,已成为定理自动证明领域的研究热点和难点.针对代数不等式提出了一种分拆降幂的机械化判定方法.首先对待证的n元不等式进行齐次化对称化处理,再通过初等对称式表示和降幂分拆,将其等价转化为具有特殊形式的一类多项式不等式,然后对多项式的系数作非负性判定.当转化后的多项式非平凡即系数不是全为非负时,则可以应用经改进的柱形分解程序BOTTEMA和QEPCAD对其作整体判定,或利用多项式完全判别系统,将其转化为一组n-2变元不等式的判定问题再进行判定.最后将此方法编制为Maple通用程序SymProve3,能够快速判定大量次数高至数百、项数数千的多元代数不等式,形成了一个以降低幂次数为主要证题特征的代数不等式判定系统.将其应用于((567 Nice and Hard Inequalities》中列出的209个多元初等不等式的证明,仅用33秒.
不等式的機器判定,因其廣汎的用途和內在的複雜性,已成為定理自動證明領域的研究熱點和難點.針對代數不等式提齣瞭一種分拆降冪的機械化判定方法.首先對待證的n元不等式進行齊次化對稱化處理,再通過初等對稱式錶示和降冪分拆,將其等價轉化為具有特殊形式的一類多項式不等式,然後對多項式的繫數作非負性判定.噹轉化後的多項式非平凡即繫數不是全為非負時,則可以應用經改進的柱形分解程序BOTTEMA和QEPCAD對其作整體判定,或利用多項式完全判彆繫統,將其轉化為一組n-2變元不等式的判定問題再進行判定.最後將此方法編製為Maple通用程序SymProve3,能夠快速判定大量次數高至數百、項數數韆的多元代數不等式,形成瞭一箇以降低冪次數為主要證題特徵的代數不等式判定繫統.將其應用于((567 Nice and Hard Inequalities》中列齣的209箇多元初等不等式的證明,僅用33秒.
불등식적궤기판정,인기엄범적용도화내재적복잡성,이성위정리자동증명영역적연구열점화난점.침대대수불등식제출료일충분탁강멱적궤계화판정방법.수선대대증적n원불등식진행제차화대칭화처리,재통과초등대칭식표시화강멱분탁,장기등개전화위구유특수형식적일류다항식불등식,연후대다항식적계수작비부성판정.당전화후적다항식비평범즉계수불시전위비부시,칙가이응용경개진적주형분해정서BOTTEMA화QEPCAD대기작정체판정,혹이용다항식완전판별계통,장기전화위일조n-2변원불등식적판정문제재진행판정.최후장차방법편제위Maple통용정서SymProve3,능구쾌속판정대량차수고지수백、항수수천적다원대수불등식,형성료일개이강저멱차수위주요증제특정적대수불등식판정계통.장기응용우((567 Nice and Hard Inequalities》중렬출적209개다원초등불등식적증명,부용33초.
