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

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