| 微分几何定理证明中最简单辅助条件的计算 |
| |
| 引用本文： | 王继民,李廉.微分几何定理证明中最简单辅助条件的计算[J].兰州大学学报(自然科学版),2003,39(1):20-23. |
| |
| 作者姓名： | 王继民 李廉 |
| |
| 作者单位： | 1. 北京大学计算机科学技术系,北京,100871;兰州大学信息科学与工程学院,甘肃,兰州,730000
2. 兰州大学信息科学与工程学院,甘肃,兰州,730000 |
| |
| 基金项目： | 国家‘973’项目“数学机械化与自动推理平台”资助项目 ( G1 9980 30 6) . |
| |
| 摘 要： | 在微分几何定理证明中，一个定理成立的辅助条件(非退化条件)不是惟一的，但越简单越好。对预先确定的标准如变元个数最少、导数算子阶数最低等，利用根微分理想分解的Rosenfeld—Groebner算法，给出了微分几何定理机器证明中最简单辅助条件的构造性算法。
|
| 关 键 词： | 微分几何定理 机器证明 吴方法 Rosenfeld—Gr6bner算法 辅助条件 构造性算法 |
| 文章编号： | 0455-2059(2003)01-0020-04 |
| 修稿时间： | 2002年3月21日 |
Computing simplest subsidiary conditions in differential geometry theorem proving |
| |
| WANG Ji-min ,Li Lian.Computing simplest subsidiary conditions in differential geometry theorem proving[J].Journal of Lanzhou University(Natural Science),2003,39(1):20-23. |
| |
| Authors: | WANG Ji-min Li Lian |
| |
| Institution: | WANG Ji-min 1,2,Li Lian2 |
| |
| Abstract: | 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. |
| |
| Keywords: | |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
