代数不等式的分拆降维方法与机器证明

利用双变元对称型所构成实线性空间的特点,设计了一种特殊形式的基,基中元素是非负的.如果一个元在此基下的坐标非负,则该元自身也是非负的.于是要证明某个元非负将被归结为证明其在指定基下的坐标非负.通常坐标中的变元数,少于原对称型的变元数,从而起到了降低维数的作用.对非对称型,可通过对称化转换为对称型来处理.根据该方法编制了Maple通用程序Bidecomp.虽此方法并非完备的,但大量的应用实例表明了此种方法证明多项式型不等式的有效性.

Method of Decreasing Dimension by Partition and Automated Proving for Algebraic Inequalities

A set of special basis in which the elements are nonnegative is designed based on the feature of real linear space generated by bivariate symmetric form. The variant itself is nonnegative if its coordinates is nonnegative under the special basis designed. Thus the proof of nonnegativity of a variant is transformed into the proof of nonnegativity of coordinates corresponding to the variant in appointed basis. And decreasing dimension is successful, for the number of variates in coordinates is always less than the number of variants belonged to symmetric form. Furthermore, we are able to solve the nonegativity of a variant belonged to unsymmetric form by transforming the unsymmetric form into the symmetric form. Finally, the general program called Bidecomp is programmed according to the above method. The method is very efficient although it is incomplete.