Tarski模型外可判定命题的机械化研究

初等代数的Tarski模型在实代数几何中起着基本的作用,然而实代数几何中也有许多重要命题在Tarski模型之外.其中比较典型的是如下命题类: 公式An中变元个数n也是变化的, 变化范围通常是正整数集.当对n赋值为具体正整数r时,公式Ar属于Tarski模型.这个命题类包含了许多重要的常用基本工具,如Cauchy不等式、Apely不等式等等.因此,研究既能适应传统理论发展需要、又能适应机械化发展需要的Tarski模型外可判定理论体系和系统方法显得特别重要．本项目拟利用降维思想与离散变量连续化思想，通过提出对称核，判定点集等基本概念，结合逐次差分代换算法,数值并行原理等,将问题转化到Tarski模型内来解决，建立完整的Tarsiki模型外可判定性理论并构造切实可行的判定算法．在理论的完整性、统一性、实用性以及方法的系统性方面，能适应数学机械化基础理论和基本方法发展需要.

本项目在国家自然科学基金(青年基金)的支持下,按照申请书拟定的计划展开研究. 先后在在Tarski模型外可判定命题和差分代换方法研究等几个方面取得了一系列研究成果.我们建立了对称核方法,广义的Schur分解方法,单纯形的等分点方法.实现了几类Tarski模型外可判定命题的机械化算法.在差分代换方法方面,我们详细研究了差分代换方法的适用范围与Pólya方法的适用范围.证明了差分代换方法比Pólya方法有更大的适用范围.并使用有限核原理完成了差分代换方法的完备化.差分代换方法为实代数的研究提供了新的工具,推动了相关领域的进一步发展.并在Copositive矩阵的判定,简单多边形分类,三角代数数的符号计算,三角不定方程求解以及程序终止性的判定等方面取得了研究成果.在本项目3年实施期间,已发表论文12篇,1篇已录用待发表,编写完成程序3个.其中SCI,EI收录论文3篇, 国内核心期刑《中国科学（数学）》，《数学学报》，《系统科学与数学》，《计算机辅助设计与图形学学报》，《软件学报》计6篇,顺利完成了研究计划所设定的研究内容和目标.