不等式基础理论公理化研究与不等式机器证明

不等式理论及其机械化原理不仅是各科学领域的理论基础，还是解决高新技术领域中的关键基础理论问题的基本工具。因此发展既能适应传统理论发展需要、又能适应机械化发展需要的不等式理论体系和系统方法显得特别的重要．本项目拟利用公理化思想和演绎推理的方法，通过提出抽象平均、抽象凸函数和抽象控制等基本概念，建立系统的抽象控制不等式理论体系，该理论为几乎所有基本不等式的统一提供了框架和模式，展示不等式理论发展的一种新的方向和趋势．在这个理论体系基础上，结合多项式完全判别系统理论和高效能降维算法原理，提出相应的高效能新降维算法，通过完成Maple平台上的编程，实现高维(次)复杂不等式型定理的机器证明与自动发现，推动不等式机器证明的发展．同时利用不等式机械化方法解决不等式理论发展中的若干关键问题．因此，开展不等式基础理论公理化与不等式机器证明的相得益彰式的基础研究具有重要的理论意义和广阔的发展空间及应用前景．

在不等式基础理论研究方面，我们建立了控制不等式公理化理论体系的框架，奠定了控制不等式研究的理论基础．获得了控制不等式分类的理论基础，结束了算术控制不等式、几何控制不等式、调和控制不等式等理论混存的局面．同时我们在积分不等式公理化理论方面取得了初步的进展．. 在不等式机器证明方面，我们获得了上齐次多项式正半定型、不定型判定的充要条件，编写的程序NEWTSDS和RESTSDS 实现其机器证明．进一步获得了齐次多项式正半定性判定的完全算法，完美地解决了GSDS判别方法完备化的问题，该结果表明：逐次差分代换方法适用范围严格大于Pólya 方法适用范围．我们的结果不仅在理论上超越了Pólya 定理，而且在方法属于构造性的，并且大量非平凡例子的机械化展示了GSDS方法强大的威力和广泛的实用价值．