《不等式基礎理論公理化研究與不等式機器證明》是依託四川師範大學，由楊定華擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：不等式基礎理論公理化研究與不等式機器證明
- 項目類別：青年科學基金項目
- 項目負責人：楊定華
- 依託單位：四川師範大學
項目摘要,結題摘要,
項目摘要
不等式理論及其機械化原理不僅是各科學領域的理論基礎，還是解決高新技術領域中的關鍵基礎理論問題的基本工具。因此發展既能適應傳統理論發展需要、又能適應機械化發展需要的不等式理論體系和系統方法顯得特別的重要．本項目擬利用公理化思想和演繹推理的方法，通過提出抽象平均、抽象凸函式和抽象控制等基本概念，建立系統的抽象控制不等式理論體系，該理論為幾乎所有基本不等式的統一提供了框架和模式，展示不等式理論發展的一種新的方向和趨勢．在這個理論體系基礎上，結合多項式完全判別系統理論和高效能降維算法原理，提出相應的高效能新降維算法，通過完成Maple平台上的編程，實現高維(次)複雜不等式型定理的機器證明與自動發現，推動不等式機器證明的發展．同時利用不等式機械化方法解決不等式理論發展中的若干關鍵問題．因此，開展不等式基礎理論公理化與不等式機器證明的相得益彰式的基礎研究具有重要的理論意義和廣闊的發展空間及套用前景．
結題摘要
在不等式基礎理論研究方面，我們建立了控制不等式公理化理論體系的框架，奠定了控制不等式研究的理論基礎．獲得了控制不等式分類的理論基礎，結束了算術控制不等式、幾何控制不等式、調和控制不等式等理論混存的局面．同時我們在積分不等式公理化理論方面取得了初步的進展．在不等式機器證明方面，我們獲得了上齊次多項式正半定型、不定型判定的充要條件，編寫的程式NEWTSDS和RESTSDS 實現其機器證明．進一步獲得了齊次多項式正半定性判定的完全算法，完美地解決了GSDS判別方法完備化的問題，該結果表明：逐次差分代換方法適用範圍嚴格大於Pólya 方法適用範圍．我們的結果不僅在理論上超越了Pólya 定理，而且在方法屬於構造性的，並且大量非平凡例子的機械化展示了GSDS方法強大的威力和廣泛的實用價值．
