微分几何定理证明中最简单辅助条件的计算  

Computing simplest subsidiary conditions in differential geometry theorem proving

作　　者：王继民[1] 李廉[2] 

机构地区：[1]北京大学计算机科学技术系,北京100871 [2]兰州大学信息科学与工程学院,甘肃兰州730000

出　　处：《兰州大学学报（自然科学版）》2003年第1期20-23,共4页Journal of Lanzhou University(Natural Sciences)

基　　金：国家‘973’项目"数学机械化与自动推理平台"资助项目 ( G1 9980 30 6) .

摘　　要：在微分几何定理证明中 ,一个定理成立的辅助条件 (非退化条件 )不是惟一的 ,但越简单越好 .对预先确定的标准如变元个数最少、导数算子阶数最低等 ,利用根微分理想分解的 Rosenfeld-Grobner算法 ,给出了微分几何定理机器证明中最简单辅助条件的构造性算法 .The subsidiary conditions (or called non-degeneracy conditions) are not one and only that a theorem holds in differential geometry theorem proving. And the simpler they are, the better. For a given standard such as the smallest variables number or the lowest order derivation operations, etc, a constructive algorithm for computing the simplest subsidiary conditions is given by using Rosenfeld-Grbner algorithm in differential geometry theorem proving in this paper.

关 键 词：微分几何定理 机器证明 吴方法 Rosenfeld—Gr6bner算法 辅助条件 构造性算法 

分 类 号：O186.1[理学—数学] O141.2[理学—基础数学]