Algorithm and Implementation of Mechanical Proving of a Class of Theorems in Elementary Differential Geometry
一类初等微分几何定理机器证明的算法与实现

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.