逐次差分代换的对偶算法

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

基于Dixon结式和逐次差分代换的多项式秩函数探测方法

秩函数探测是循环程序终止性分析的重要方法,目前,已有很多研究者致力于为线性循环程序探测对应的线性秩函数,然而,针对具有多项式循环条件和多项式赋值的多项式型的循环,现有的秩函数探测方法还有所不足,解决方案大多是不完备的、或者具有较高的时间复杂度。针对现有工作对于多项式秩函数探测方法不足的问题,基于扩展Dixon结式(KSY方法)和逐次差分代换(SDS)方法,提出一种为多项式循环程序探测多项式型秩函数的方法。首先,将待探测的秩函数模板看作带参数系数的多项式,将秩函数的探测转换为寻找满足条件的参数系数的问题;然后,进一步将问题转换为判定相应的方程组是否有解的问题,至此,利用KSY方法中的扩展的Dixon结式,将问题更进一步简化为带参系数多项式(即结式)严格为正的判定问题;最后,利用SDS方法,找到一个充分条件,使得得到的结式严格为正,此时,可以获取满足条件的参数系数的取值,从而找到一个满足条件的秩函数,通过实验验证该秩函数探测方法的有效性。实验结果表明,利用该方法,可以有效地为多项式循环程序找到多项式秩函数,包括深度为d的多阶段多项式秩函数,与已有方法相比,该方法能够更高效地找到多项式秩函数,对于基于柱形代数分解(CAD)方法的探测方法因时间复杂度问题无法而应对的一些循环,利用所提方法能够在几秒内为这些循环找到秩函数。

利用改进的逐次差分代换证明多项式正半定性

近年来由杨路等提出了一种利用逐次差分代换以证明多项式非负性的方法,并在MAPLE平台编写了相应程序。但是,对于某些多项式的非负性却无法在一定时间内给出有效证明。文章改进了逐次差分代换的判定方法,可以较好的解决这一类问题。

基于列随机矩阵的逐次差分代换与正半定型的机械化判定

本文选择列随机平均矩阵Tn作为基本代换矩阵，建立了基于％的逐次差分代换方法．获得了腿翌上正半定型，不定型判定的充要条件．并进一步证明了：正定型的差分代换集序列正向终止．根据这些结果编写的Maple程序TSDS3，能够自动证明代数型不等式，对不成立的不等式总能输出反例．该程序虽可能不停机，但大量的应用实例证实了该方法的实用性．

Pólya方法与逐次差分代换方法

通过检查某些特定型系数的非负性来证明给定型非负性的方法中,最典型的是Pólya方法与基于重心矩阵的逐次差分代换方法(GSDS).本文完整地比较了这两种方法的适用范围,证明了型f如果可使用Pólya方法证明非负性,则GSDS方法也可以,但反之不然.即GSDS方法的适用范围严格大于Pólya方法的适用范围.

基于差分代换的正半定型判定完备方法

研究并发展逐次差分代换方法,得到R n+上正半定型差分代换次数的一个上界。由此获得判定R n+上正半定型的充要条件。根据此充要条件建立的算法是必定能终止的。同时提出一类新的差分代换矩阵。

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

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

用增量分拆法证明齐次多项式不等式

针对差分代换证明齐次多项式不等式存在的困难和问题,提出了一种解决方法,并对Bottem a软件和一般多项式差分代换DS(F)进行了评价。