一类初等微分几何定理机器证明的算法与实现  

ALGORITHM AND IMPLEMENTATION OF MECHANICAL PROVING OF A CLASS OF THEOREMS IN ELEMENTARY DIFFERENTIAL GEOMETRY

作　　者：曹丽娜[1] 李洪波[2] 

机构地区：[1]中央民族大学数学与计算机科学学院,北京100081 [2]中科院数学与系统科学研究院数学机械化重点实验室,北京100080

出　　处：《系统科学与数学》2006年第4期395-401,共7页Journal of Systems Science and Mathematical Sciences

基　　金：国家自然科学基金(10471143);中央民族大学"十五"重点项目(10502C05)资助课题

摘　　要：空间曲面上的曲线论是初等微分几何的重要部分．作者提出了一种以外微分运算和向量计算为主要工具,可以进行有关曲面上曲线局部性质的定理机器证明的算法．该算法结合了曲面上的活动标架,曲面上曲线的测地标架和曲线自身的Frenet标架,在Maple 9下得到实现．对20个例子进行的测试表明,由该算法生成的自动证明简短可读．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.

关 键 词：定理机器证明 曲面上的曲线 外微分运算 向量计算 

分 类 号：O186.11[理学—数学]