| 一类初等微分几何定理机器证明的算法与实现 |
| |
| 引用本文： | 曹丽娜,李洪波.一类初等微分几何定理机器证明的算法与实现[J].系统科学与数学,2006,26(4):395-401. |
| |
| 作者姓名： | 曹丽娜 李洪波 |
| |
| 作者单位： | 1. 中央民族大学数学与计算机科学学院,北京,100081
2. 中科院数学与系统科学研究院数学机械化重点实验室,北京,100080 |
| |
| 基金项目： | 国家自然科学基金(10471143)，中央民族大学“十五”重点项目(10502C05)资助课题 |
| |
| 摘 要： | 空间曲面上的曲线论是初等微分几何的重要部分．作者提出了一种以外微分运算和向量计算为主要工具,可以进行有关曲面上曲线局部性质的定理机器证明的算法．该算法结合了曲面上的活动标架,曲面上曲线的测地标架和曲线自身的Frenet标架,在Maple 9下得到实现．对20个例子进行的测试表明,由该算法生成的自动证明简短可读．
|
| 关 键 词： | 定理机器证明 曲面上的曲线 外微分运算 向量计算 |
| 修稿时间： | 2005年5月12日 |
Algorithm and Implementation of Mechanical Proving of a Class of Theorems in Elementary Differential Geometry |
| |
| Cao Lina,Li Hongbo.Algorithm and Implementation of Mechanical Proving of a Class of Theorems in Elementary Differential Geometry[J].Journal of Systems Science and Mathematical Sciences,2006,26(4):395-401. |
| |
| Authors: | Cao Lina Li Hongbo |
| |
| Institution: | (1)School of Mathematics and Computer Science, Central University for Nationalities, Beijing 100081; (2) KLMM, AMSS, Academia Sinica, Beijing 100080 |
| |
| Abstract: | The theory of curves on space surfaces is an important part of the theory of elementary differential geometry. In this paper, a mechanical theorem proving algorithm is proposed, which is based on the exterior differential calculation, vector formulation and the integration of the moving frames of the surfaces, geodesic frames and Frenet frames of the curves on the surfaces. The algorithm is applicable to theorems on local properties of curves on space surfaces, and has been implemented with Maple 9 and tested by 20 examples. |
| |
| Keywords: | Mechanical theorem proving curves on space surfaces exterior differential calculation vector formulation |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《系统科学与数学》浏览原始摘要信息 |
| 点击此处可从《系统科学与数学》下载免费的PDF全文 |
|
