差分代换与不等式机器证明

设计了一个试探性的计算机程序SDS,用于证明多项式不等式,或等价地,用于判定多项式的非负性.将各变量按一定方式分割成较小的非负量,将变量替换后的多项式合并同类项,然后看是否所有的系数都是非负的.该方法不是完备的,但实验结果表明该程序对许多情况有效.不少次数较高或变量较多的多项式,除了SDS,还没有任何其他软件能做.

一类根式不等式的有理化算法与机器证明

文中讨论了一类根式不等式的有理等价问题.证明了这类根式不等式可等价转化为一组有理不等式.建立了一个算法RFD,并用Maple编程实现.对一个给定的这类根式不等式,RFD可自动快速地产生一组有理等价不等式.将RFD算法和差分代换方法相结合,给出了一大类具有相当难度的几何不等式的机器证明.此前该课题仅有的工作是杨路关于二次根式的结果.

逐次差分代换的对偶算法

逐次差分代换算法(SDS)在不等式机器证明领域是有力工具.原来的逐次差分代换算法虽然可以被应用于带有逻辑连词"∧"(and)类型的不等式命题,但是不能应用于带逻辑连词"∨"(or)类型不等式命题.主要工作是发展出了逐次差分代换的对偶算法(DASDS).新建立的对偶算法不仅克服了上述困难,甚至对某些带有量词""的不等式命题也是有效的.使用改进后的算法,一个公开的根式不等式问题被解决.

基于随机矩阵的差分代换算法的完备化

本文利用有限核原理,给出了基于随机矩阵的逐次差分代换方法的一个完备化.获得了判定多项式半正定性的完全算法.此算法可进一步应用于计算有理函数的全局最优值.与常用的数值最优化方法不同的是,本方法获得的是精确符号解.