基于列随机矩阵的逐次差分代换与正半定型的机械化判定  

Infinite product convergence of column stochastic mean matrix and machine decision for positive semi-definite forms

作　　者：姚勇[1] 

机构地区：[1]中国科学院成都计算机应用研究所,成都610041

出　　处：《中国科学：数学》2010年第3期251-264,共14页Scientia Sinica：Mathematica

基　　金：国家重点基础研究发展规划(批准号:2004CB318003);国家自然科学基金(批准号:90718041;10901116);中国科学院知识创新工程重要方向(批准号:KJCX-YW-S02)资助项目

摘　　要：本文选择列随机平均矩阵Tn作为基本代换矩阵，建立了基于％的逐次差分代换方法．获得了腿翌上正半定型，不定型判定的充要条件．并进一步证明了：正定型的差分代换集序列正向终止．根据这些结果编写的Maple程序TSDS3，能够自动证明代数型不等式，对不成立的不等式总能输出反例．该程序虽可能不停机，但大量的应用实例证实了该方法的实用性．First we define the column stochastic mean matrix, and then prove that if we choose countable infinite matrices from finite n x n column stochastic mean ones at random （repeats allowed）, then the product of these infinite matrices will converge to a column stochastic mean matrix with rank 1. Finally we show the proof for relations between the termination of the sequence of SDS sets and positive semi-definite property of a form. This method is verified to be very efficient and better than Polya method.

关 键 词：逐次差分代换 差分代换集序列 终止性 正半定型 机械化判定 

分 类 号：O178[理学—数学] O211.1[理学—基础数学]