实轮换对称型及其半正定性判定的可读证明  

READABLE PROOF TO THE DETERMINATION OF THE POSITIVE SEMI-DEFINITENESS OF REAL CYCLIC SYMMETRIC FORM

作　　者：陈胜利[1] 黄方剑[2] 

机构地区：[1]中国科学院成都计算机应用研究所,成都610041 [2]电子科技大学能源科学与工程学院,成都611731

出　　处：《系统科学与数学》2012年第8期986-1001,共16页Journal of Systems Science and Mathematical Sciences

基　　金：中国科学院知识创新工程资助项目(KJCX-YW-S02)

摘　　要：可读证明是不等式机器证明领域中的热点问题.针对具有对称零点的实轮换对称型,文章提出了其线性空间的一组基以及分拆算法和两种分拆形式用于对不等式进行可读证明研究.讨论了该线性空间的维数,以及轮换对称型半正定性的判别方法.给出了一类具有对称零点的轮换对称型的半正定性判定条件.大量实例表明此分拆方式在轮换对称型半正定性的判定及可读证明上具有很好的实用性.The readable proof to inequalities is a new approach in mathematics mechanization. According to the linear space composed of real cyclic symmetric tbrms with symmetric zero, we provide one base, a decomposition algorithm and two decomposition methods of this space. First, we discuss the dimension of this space and then give a way to determine the positive semi-definiteness of cyclic symmetric forms. In the last section, some examples are given to show the efficiency of our method.

关 键 词：轮换对称型 对称零点 可读证明 半正定性判定 

分 类 号：O177.3[理学—数学]