论文部分内容阅读
本文主要讨论微分几何符号计算和初等微分几何的定理机器证明两个方面的问题。考虑微分几何符号计算这个问题的主要动机来源于：(1)微分几何定理机器证明集中体现在运用数学符号的代数运算来进行几何定理的自动推理。(2)空间上曲面的曲线论是初等几何中的重要部分。第一章介绍了数学机械化的思想与计算机代数，回顾了几何定理机器证明的历史和发展。第二章介绍了微分几何曲线、曲面的基本知识和定理，建立一个统一的符号系统以便进行微分几何定理的机器证明。第三章提出了使用微分形式和活动标架作为基本的代数工具进行空间曲面和空间曲线局部定理的机器证明方法，将曲面的活动标架和曲面上曲线的测地标架曲线自身的Frenet标架结合起来，进行曲面上曲线的局部定理机器证明，给出了以使用外微分运算，和向量计算为主要工具的曲面上曲线局部定理机器算法，在数学软件Maple10的编程环境下实现了算法。