（应用数学专业论文）微分几何曲面上曲线定理的机器证明.pdf

大连理工大学硕e 学位论文 摘要 本文主要讨论微分几何符号计算和初等微分几何的定理机器证明两个方面的问题。 考虑微分几何符号计算这个问题的主要动机来源于： ( 1 ) 微分几何定理机器证明集中体现在运用数学符号的代数运算来进行几何定理的 自动推理。 ( 2 1 空间上曲面的曲线论是初等几何中的重要部分。 第一章介绍了数学机械化的思想与计算机代数，回顾了几何定理机器证明的历史和 发展。 第二章介绍了微分几何曲线、曲面的基本知识和定理，建立一个统一的符号系统以 便进行微分几何定理的机器证明。 第三章提出了使用微分形式和活动标架作为基本的代数工具进行空间曲面和空间 曲线局部定理的机器证明方法，将曲面的活动标架和曲面上曲线的测地标架曲线自身的 f r e n e t 标架结合起来，进行曲面上曲线的局部定理机器证明，给出了以使用外微分运算， 和向量计算为主要工具的曲面上曲线局部定理机器算法，在数学软件m a p l e l o 的编程环 境下实现了算法。 关键词：机器证明；曲面；曲线：活动标架：外微分 微分几何曲面上曲线定理的机器证明 m e c h a n i c a lt h e o r e mp r o v i n go i lc u r v e so ns p a c es u r f a c e st h e o r e mo f d i f f e r e n t i a lg e o m e t r y a b s t r a c t i nt h i sp a l e r , w ed i s c u s st w op r o b l e m s o n ei sa b o u ts y m b o l i cc o m p u t a t i o ni nt h e d i f f e r e n t i a lg e o m e t r y ，a n dt h eo t h e ri sa b o u tt h em e c h a n i c a lt h e o r e mp r o v i n gi ne l e m e n t a r y d i f f e r e n t i a lg e o m e 仃y t h em o t i v a t i o no f s t u d y i n g b o t ho f t h ep r o b l e m sc o m e sf r o m ： ( 1 ) m e c h a n i c a lt h e o r e mp r o v i n gi n d i f f e r e n t i a l g e o m e t r ya i m s a t s y m b o l i z i n g m a t h e m a t i c a lr e a s o n i n g ； ( 2 ) 1 1 1 ct h e o r yo fc u r v e so ns p a c es u r f a c e si sa ni m p o r t a n tp a r to ft h et h e o r y o f e l e m e n t a r yd i f f e r e n t i a lg e o m e t r y c h a p t e r li sd e v o t e dt oi n v e s t i g a t i n gt h ei d e a so fm a t h e m a t i c sm e c h a n i z a t i o na n d c o m p u t e ra l g e b r a ；r e v i e w i n gt h eh i s t o r ya n dd e v e l o p m e n to fm e c h a n i c a lt h e o r e mp r o v i n gi n g e o m e t r y c h a p t e r2i sd e v o t e dt oi n v e s t i g a t i n gt h eb a s i ct h e o r ya n dt h e o r e mo f c u r v ea n ds u r f a c e ， e s t a b l i s h i n gau n w e 硌a ls y m b o l i ca l g e b r a i cs y a e mf o rg e o m e t r i ci nd i f f e r e n t i a lg e o m e t r y i nc h a p t e r3 ，am e c h a n i c a lt h e o r e mp r o v i n ga l g o r i t h mi sp r o p o s e d ，w h i c hi sb a s e do n t h ee x t e r i o rd i f f e r e n t i a lc a l c u l m i o n ，v e c t o rf o r m u l a t i o na n dt h ei n t e g r a t i o no ft h em o v i n g f r a m e so f t h es u r f a c e s g e o d e s i cf l a m e sa n df r e n e tf r a m e so f t h ec u r v e so nt h es u r f a c e s 1 r h e a l g o r i t h mi sa p p l i c a b l et ot h e o r e m so i ll o c a lp r o p e r t i e so fc u i v 嚣o ns p a c es u r f a c e s , a n dh a s b e e ni m p l e m e n t e dw i t hm a p l e l 0 k e yw o r d s ：m e c h a n i c a lt h e o r e mp r o v i n g , c u r v e so ns p a c es u r f a c e s , e x t e r i o rd i f f e r e n t i a l c a l c u l a t i o n ，m o v ef r a m e l i 独创性说明 作者郑重声明：本硕士学位论文是我个人在导师指导下进行的研究工 作及取得研究成果尽我所知，除了文中特别加以标注和致谢的地方外， 论文中不包含其他人已经发表或撰写的研究成果，也不包含为获得大连理 工大学或者其他单位的学位或证书所使用过的材料与我一同工作的同志 对本研究所做的贡献均已在论文中做了明确的说明并表示了谢意 作者签名：翌叠翌日期：2 竺9 。 _ 力 大连理：e 大学硕，上_ _ f 叶究生学位论文 大连理工大学学位论文版权使用授权书 本学位论文作者及指导教师完全了解“大连理工大学硕士、博士学位 论文版权使用规定”，同意大连理工大学保留并向国家有关部门或机构送 交学位论文的复印件和电子版，允许论文被查阅和借闯。本人授权大连理 工大学可以将本学位论文的全部或部分内容编入有关数据库进行检索，也 可采用影印、缩印或扫描等复制手段保存和汇编学位论文。 作者签名：至堑 一名：燃 硼强厂月弘曰 人连理工人学硕士学位论文 1 绪论 在1 9 7 9 年，吴文俊先生开创了初等几何定理机器证明，建立了著名的吴方法 1 。 在之后的十几年，该方法被用来进行曲线论，曲面论、经典力学和天体力学中上百个定 理的自动证明和发现1 9 9 3 年， 2 提出了在一维的情况下r i t t - w u 良序原理的一个改 进，减少了特征集的分支数目1 9 9 5 年， 3 受s e id e n b e r g 消去理论的启发，提出了零 点分解的新方法，可以提高吴方法在空间曲线定理机器证明方面的效率同年， 4 进行 了空间曲面定理机器证明的研究，通过计算曲面基本方程的特征集，发现了一个新的定 理1 9 9 8 年， 5 提出了c 1 i f f o r d 代数约化的方法，用来进行空间曲线局部定理证明的 自动推理这个方法是在常微分多项式的r i t t - w u 良序原理，欧氏几何的c l i f f o r d 代数 表示和c i i f f o r d 代数求解向量方程( 组) 的公式基础上建立起来的。1 9 9 7 年，e 6 2 提出了 一个基于外微分运算和吴方法的自动推理方法来处理局部曲面论的闻题，并且应用这一 方法给出了关于w e i n g a r t e n 曲面的陈省身定理的自动证明。 在以上工作的基础之上，本文运用活动标架和外微分理论把曲面上的曲线运算归结 为一类统一的问题，并结合了曲面和曲线自身的性质，在m a p l e l o 工具中实现了曲面上 的曲线的测地曲率，测地挠率，法曲率，曲线自身的曲率，挠率和曲率线相关的内容的 计算和证明。 1 1 数学机械化与计算机代数 十六、十七世纪以来，人类历史上经历了一场史无前例的技术革命，出现了各种类 型的机器，取代各种形式的体力劳动，使人类进入一个新时代。几百年后的今天，电子 计算机已开始有条件地代替一部分特定的体力劳动，因而人类已面临另一场更宏伟的技 术革命，处在又一个新时代的前夕。数学在这场新的技术革命中，无疑将扮演一个重要 的角色。与工业革命相适应出现了解析几何与微积分这些数学上的伟大创新。在目前这 一以计算机为标志的信息革命时代，数学应该有什么样的创新与之相适应呢? 正是基于 这种考虑，我国著名数学家，首届国家最高科技奖获得者之一，吴文俊院士 7 倡导数 学机械化研究。 所谓机械化，无非是刻板化和规格化，机械化的动作，由于简单刻板，因而可以 让机器来实现，又由于往往需要反复千百万次，超出了人力的可能，因而又不能不让机 器来实现因之，机械化为机器化进而自动化铺平道路，是它们必不可少的前奏就这一 意义来说，数学中的某些脑力劳动与体力劳动颇有共同之处，它们也同样可以机械化。 微分儿何曲面上曲线定理的机器证明 历史上公理化的思想与机械化的思想彼此辉映，贯穿于整个数学历史，对数学的发 展都起到了巨大的作用。前者是在现代数学一尤其是纯粹数学中占统治地位的，但是后 者也同样发挥了极其重要的作用。如：希尔伯特( h i l b e r t ) 所倡导的数理逻辑，为日计算 机设计原理的发展奠定了基础。数学巨匠嘉当( e c a r t a n ) 在微分方程，微分几何及李群 ( l i e6 r o u p ) 的著作中体现了机械化思想的特色。h c a r t a n 关于代数拓扑中同调群计算 的工作也可视为机械化思想的成功典范。 2 0 世纪7 0 年代，中国科学院院士吴文俊先生由中国的传统思想出发，从几何定理 证明入手始数学机械化研究，所建立的数学机械化方法不仅将中国传统数学发扬光大， 而且也为国际自动推理的研究开辟了新的前景1 9 7 8 年，吴先生在中国科学上发表 了题为初等几何判定闯题与机械化原理的论文 8 ：1 9 8 4 年，吴先生的学术专著几 何定理机器证明的基本原理由科学出版社出版，这部专著建立了各类几何的机械化定 理，阐明几何定理机械化证明的基本原理。1 9 8 5 年，吴先生的论文关于代数方程组的 零点发表 9 ，具体讨论了多项式方程组所确定的零点集。这篇重要文献，是正式建 立求解多元多项式方程组的吴文俊消元法的重要标志。自此“吴方法”宣告诞生，数学 机械化研究揭开新的一页。”m c c a r t h y 程序验证奖”得主j s m o o r e 认为，吴先生的工 作“不仅奠定了自动推理研究的基础，而且给出了衡量其它推理方法的明确标准”：“在 吴方法建立以前，定理机器证明的研究处于一片茫然之中，吴不仅冲破了这种沉寂的局 面，而且带来了极为光明的前景”。 1 9 8 9 年。在r i t t 1 0 等人工作的基础上，吴先生将吴代数消元法的思想推广到微 分情形，创立了吴微分消元法 1 1 ，提出了吴微分特征列的概念，完善和发展了特征集 理论。高小山研究员、张景中院士、周成青教授 1 2 - 1 6 合作提出了基于几何不变量的 “消点法”，实现了自动生成几何定理可读证明这一目标。依据这一方法编制的程序已 经用于证明了数百条定理。这一工作被认为是五十年g e r l e n t n e r 的经典工作及七十年 代吴方法以来这一领域又一重要进展。美国数学会“自动定理证明成就奖”及 “j m a c a r t h e y 程序验证奖”得主b o y e r 称该工作“是自( 五十年代s l a g l e 和m o s e s 符号积分程序以来自动推理界最重要的一件单独的事情”。该工作“在使计算机象具有 算术天才那样具有几何天才这一不可避免的过程中将是一座里程碑”，自动推理届权威 l o v e l a n d 在a im a n a z i n e 的文章中将这一工作列为近年来推动推理界“重要进展”的第 一项。称“在儿何中证明有意义的定理并给出可读证明( 6 e l e n t n e r 五十年代的重要工 作) ”近年来才由周咸青，高小青，张景中的几何定理证明器超过。”在几何自动推理 方面，他们提出了微分几何的自动定理证明的新方法所编程序自均证明了上百个定理并 一2 一 大连理工大学硕士学位论文 发现了新结果给出了c a l e y k l e i n 几何的转换定理，大大简化了非欧几何的自动定理 证明：解决了z a s s e n t a a u 与m a c l a n e 公开问题：提出了几何推理的演绎数据库方法：改进 了基于搜索的定理证明方法，并第一次用此类方法证明了大量几何定理。 李洪波研究员、程民德教授 1 7 提出了基于c l i f f o r d 代数与吴方法的向量算法， 这一算法不仅可以用来证明初等几何定理，还可以证明微分几何中的定理。 计算机与应用数学的结合可以分为两个层面：数值计算与符号计算。数值计算的内 容是实数演算，更确切地说，数值计算是寻找适当的有理数去逼近实际问题的实数解。 这类实际问题往往通过微分、积分或者其他类型的方程组以及适当的初边值条件来表 达。因为计算不可能准确地表达实数，所以通过数值计算得到的结果是近似的符号计 算，顾名思义，是在计算机上依符号的形式进行计算，实现公式的机器推演，符号计算 的结果是精确的 计算机代数兴起于上世纪6 0 年初。是介于计算机，数学与人工智能之间的一门边 缘学科。计算机代数的主要研究内容是计算机上数学公式演绎的算法和系统应用其发 展。大致可分为以下几个阶段 1 8 。 1 2 0 世纪6 0 年代：发展初期，着重于多项式算术，积分方法： 2 2 0 世纪7 0 年代：诞生了m a c s y m a ，r e d u c e ，以及用于抽象域的s c t w t c h p a d 1 i ： 3 2 0 世纪8 0 年代：多项式时间方法，因式分解等的研究，m a p l e 与m a t h e m a t i c a 相续发布。 4 2 0 世纪9 0 年代：微积分，数学的w e b 发布，黑箱符号对象： 5 本世纪初：符号计算，数值计算，几何，组合与逻辑范例的融合 计算机代数的主要功能在于：在计算机上以符号形式进行运算，实现公式的机器推 演。如果和初等数学相比，寻常的数值计算可比拟为数值计算，而符号计算可比拟为代 数运算( 故有计算机代数之说) 。前者只适合于个例分析，后者的结果则具有普遍性。由 于计算机代替了人工的推导，演算速度成千万倍地增加，使得原来令人望而生畏的复杂 计算变得简易快洁。在最初的十几年间，计算机代数也被叫做：符号与代数计算、公式 处理、机器代数等。于是在1 9 7 9 年，美国加州理工学院的e e g 教授统一了计算机代 数的名称和定义：“计算机代数是一门利用数学、计算机进行代数和解析处理或操作的 学科”1 9 8 2 年，德国卡尔斯鲁厄大学的r l o o s e 教授又进行了进一步的拓广和补充： “计算机代数是设计、分析、改造和应用代数算法的计算机科学分支”。计算机代数的 最早出现公认以1 9 6 0 年美国麻省理工学院的m c c a r t h y 推出的l i s p 语言为标志在随后 的十几年间，计算机代数的发展引起了国际计算机科学界的重视美国的计算机协会组 织了符一号与代数处理一专业组( s p e c i a li n t e r e s tg r o u po ns y m b o l i ca n da l g e b r a i c 微分几何曲面上曲线定理的机器证明 m a n i p u l a t i o n 。简称s i g s a m ) ，其成员遍布世界3 0 多个国家。这个国际组织每两年召开 一次国际会议( 简称i s s a c ) ，专门交流计算机代数方面的研究成果。西欧各国计算机工 作者组织了欧洲符号和代数处理专业委员会( s y m b o l i ca n da l g e b r a i cm a n i p u l a t i o no f e u r o p e a n ，简称s a m e ) ，定期召开简称a a e c c 的国际会议。这两大组织还分别创办了计 算机代数刊物s i g a mb u l l e t i n 和j o u r n a lo fs y m b o l i cc o m p u t a t i o n 这些学术活动大 大地推动了计算机代数的发展。 符号计算软件的发展大体经历了三个阶段：上个世纪6 0 年代的专门化程序：7 0 年代 的通用程序和8 0 年代至今的商业化程序。1 9 6 0 年，用于表处理的计算机语言l i s p 在美 国开发成功。l i s p 在符号计算软件中起了重要作用j a m e ss l a g l e 写的第一个符号积分 程序以及稍后由j o e lm o s e s 写的符号积分程序都是用l i s p 写成的。1 9 7 1 年，第一个基 于l i s p 的通用符号计算软件m a c s y m a 间世，它提供了计算极限和解方程的功能a c h e a r n 用l i s p 开发了符号计算系统r e d u c e ，后来成为一个广泛应用的通用软件另 一个广泛应用的通用软件是用c 语言写成的m a p l e 。与其它符号计算系统比较，m a p l e 的效率比较高， 这是由其自身的设计特点决定的。m a p l e 系统的核心由进可能小的关于基本运算的程序 组成，这些运算包括：指令函数，整数，有理数和多项式运算以及空间管理。该软件的 其它部分是由m a p l e 语言写成的软件包。这些软件包的管理很灵活，用户，可以加入， 改变和删除函数。目前m a p l e 已有大量专用软件包。最引人注目的商业系统是由s t e p h e n w o l f r a m 组织编写的m a t h e m a t i c a ，该系统是用c 语言写成的，有很新颖的特点。例如： “代数发动机”和用户接口有本质的区别：综合了符号计算，数值计算和作图功能：具有 结构清晰的用户编程语言等。与其它系统相比，m a t h e m a t i c a 不仅成功吸引了很多学术 界以外的注意，也得到了大量用户的支持从上个世纪6 0 年代至今，各类符号计算软 件曾出不穷，各有特色，为相关学科研究提供了极大的方便。 众多用户多年来的经验证明符号计算软件有诸多优点： l 、它使用户避免大量的繁琐计算。利用符号计算软件，用户可以把繁琐复杂的计 算交给计算机，而集中精力研究用什么样的算法解决问题。 2 、它使用户容易使用先进的的数学技术( 例如：因式分解，符号积分，吴方法等) 。 通用的符号计算软件不仅有操作符号计算的能力，而且还实现了很多强有力的和复杂的 算法。 3 、它帮助研究者完成大量繁琐运算的证明。倒如：四色定理的证明，为了得到结论， 需要验证大约2 0 0 0 多种地图满足某些性质，这只能通过计算机来完成。 大连理工大学硕士学位论文 4 、它帮助研究者通过大量例子进行试验，验证猜想。 5 、它使一些古老的数学问题获得新生。例如：大整数的素数判定和分解，该问题在 编码理论中有重要应用。 6 、它促使研究者改进已知的算法和发明新算法。 当然符号计算软件也有其不足之处，主要表现在： l 、计算机代码的局限性。利用符号计算软件时，常会遇到时间和空间的限制，其 原因部分在于运用的是准确运算和符号表达式，部分在于缺乏有效的算法。 2 、中间表达式膨胀使用符号计算软件时一个常见的也是最严重的问题就是中间表 达式膨胀 1 9 。中间表达式的规模与输入表达式的规模之间的关系可能是线性的，也可 能是指数的甚至是双指数的例如，对于辗转伪除法( “无分式”除法) ，他们之闻的关 系是指数型的。 3 、输出难于管理。用户可能发现系统会返回难于处理的大型输出。例如一般4 次 多项式的完全解集，其公式会超出整个屏幕。 4 、可靠性。软件中所含的错误是一个重要的问题。大多数通用系统的基本运算， 如大多数加法和乘法，都是非常可靠的，但是关于复杂算法的软件，很可能有错误。 随着计算机代数的发展和计算机性能的改进，符号计算软件必然会越来越趋向于成 熟。尽管如此作为符号计算软件的用户，仍然有必要追求算法上的创新，从而进一步提 高符号计算的效率。 1 2 微分几何机械证明发展过程 1 2 1 吴方法的基本思想简介 在数学里要求证明的问题，往往是由条件和结论两部分所组成。所谓数学证明，众 所周知，就是根据所给的条件，已有的定义、公理以及已被证明成立的定理，按照一定 的推理格式导出结论。这在相当大的程度上要依赖于人们的智慧，才能和经验，并且需 要较长的时闻致使人们望而却步。几何定理的证明更是这样，吴文俊教授认为，我国几 何学的发展是始终与数量关系形影不离的。现代几何学的许多重要领域，例如微分几何 与代数几何，往往一开始就假定了一个数系( 一般是一个数域，甚至是一个特殊的实数 域或复数域) ，由此构成仿射空间或投影空间，然后用坐标或以函数与导数间的关系来 引进各种几何图形，如曲线、曲面及其几何关系等。看来，在数的基础上建立起整个几 何学的体系这已是大势所趋，但也不能不考虑几何学的直观背景与来源，以及它的基础 问题。如何从原始的现实形象提炼出一套几何学的公理系统，又如何从公理系统发展成 坐标系统，使几何定理的证明完全化成代数问题，使代数方法得以在几何上发挥作用， 微分几何曲面上曲线定理的机器证明 看起来是平凡的，但作起来也并非轻而易举之事。首先，因为解决这些代数问题计算量 过大。使人望而却步：其次，由于代表几何关系而出现的那些代数式往往杂乱无章，使 人们无所措手幸而现在出现了电子计算机，对繁杂的计算已经有了有效的处理办法。 因此，如何把杂乱无章的代数关系处理得井然有序，使计算机得以在证明几何定理上发 挥威力，便成为问题的关键所在。对此，吴文俊证明了如果一种几何的附属数系是一个 数域，即乘法是可以交换的，则假设与终结部分都可由多项式等式关系来表达的那类定 理的证明都可以机械化。这一类定理称为等式型定理。它的机械化问题可归结为一个纯 代数式的机械化问题。包括了几何学中最主要的大部分定理事实上，有序或无序的常 用几何学、投影几何学、非欧几何学等，它们的几何定理都有机械化证法。因此，在理 论上，这些几何学的定理证明都可以借助于计算枫来实现对此，吴文俊教授已出版 了几何定理机器证明的基本原理( 初等几何部分) 2 0 2 1 ，把几何定理的机器证明 分成以下三个步骤： ( 1 ) 几何的代数化与坐标化，从几何的公理系统出发，引进数系统与坐标系统，使 任意几何定理的证明问题成为纯代数问题； ( 2 ) 几何的机械化，将几何定理假设部分的代数关系式进行整理，然后依确定步骤 验证定理终结部分的代数关系式是否可以从假设部分已整理成序的代数关系式中推出； ( 3 ) 用计算机作最后验证，依据第二部中所确定的步骤编成程序，并在计算机上实 施，以得出定理是否成立的最后结论。 由于现在的计算机尚只能识别有限的事物，因此几何定理机器证明的一个先决条件 是第二步中所确定的代数关系式必须是以有限的形式出现。例如这些代数关系式都是以 多项式的形式出现，且其系数都是整数，则对于计算机的使用只是依据第二步中所确定 的步骤编制程序的问题，不会有任何实质性的困难。如果一门几何可以找到这样三个步 骤( 事实上只要前两个步骤即可) 来完成定理的证明，我们就说这门几何可以机械化，并 把可以机械化的这一结论称为机械化定理由以上所述可以看出，由公理化到机械化大 体上经历了如下一个过程 3 8 】： 公理化一) 代数化一) 坐标化一 机械化 一门几何学能否机械化并不显然按吴方法，几何的公理、定理与证明，实质上都 可以用有限次的构造步骤来叙述以至完成，这也就为我们提供了几何定理证明有可能机 械化的依据。吴文俊证明了：奠基于各种公理系统的每种初等几何学，只要相当于乘法 交换律的某一公理成立( 即乘法是可以交换的) ，则假设与终结部分都可以由多项式等式 表达的那类定理的证明，大都可以机械化。这些几何定理的证明，可以借助于计算机来 一6 一 大连理工大学硕士学位论文 实现，这一类定理即前面说过的等式型定理。可以机械化的几何包括了多种有序或无序 的常用几何学( 即欧氏几何的那种初等几何) ，投影几何、非欧几何与元几何等。 以上说的几何定理证明了机械化，其寻求的是一般方法，不仅适用于个别的定理， 而且适用于整个某一类型的定理，甚至可以说是某一种几何的所有定理，只要依照上述 的方法进行有限步之后，就可以对整个某一定理得到统一的证真或证伪而无分难易，其 中几何的代数化乃是关键之一步。 值得提出的是，吴方法不仅能证明几何定理，而且在其他数学领域或物理学科上也 大有用场 2 2 例如还以推广到代数几何等领域。美国数学家乌拉，为了要探讨应用中 广泛出现、而现代数学又对之还无能为力的非线性现象，便是在计算机上进行试验。发 现了一些规律。近年来，微分方程孤立子解的获得，就是首先在计算机的荧光屏上发现 的。这是应用数学上的一个重大突破，吴文俊教授本人还曾利用他的方法，在开普勒定 律之下，成功地证明了著名的万有引力定律。 1 2 2c li f f o r d 代数，几何计算和几何推理 数学历史上，c l i f f o r d 代数 2 3 是一种深深根植于几何学之中的代数系统，被它的 创始人称为几何代数。历史上e c a r t a n 2 4 ，r b r a u e r 2 5 ，h w e y l ， c c h e v e l l y 2 p 2 7 1 等大师都研究过c 1 i f f o r d 代数，对它的发展起了重要作用近年来， c l i f f o r d 代数在微分几何、理论物理、经典分析等方面取得了辉煌的成就，是现代理论 数学和物理的一个核心工具，并在现代科技的各个领域，如机器人学、信号处理、计算 机视觉、计算生物学、量子计算等方面有广泛的应用。 c l i f f o r d 代数在几何计算和几何推理中的应用尤为突出。作为一种优秀的描述和计 算几何润题的代数语言，c l i f f o r d 代数对于几何体，几何关系和几何变换有不依赖于坐 标的、易于计算的多种表示的特点，因而应用它进行几何自动推理，不仅使困难定理的 证明往往变得极为简单，而且能够解决一些著名的公开问题目前在国际上，几何自动 推理已经成为c l i f f o r d 代数的一个重要应用领域。 由吴文俊先生开创的数学机械化领域，其核心内容是证定理、解方程，它建立于深 刻的数学基础之上欧美学者用于机器证明的6 r o b n e r 基方法建立于理想论基础上，是 纯粹代数的方法：吴方法则是建立在代数几何和特征列理论基础上，是几何观念和代数 工具的结合这一区别，是我国吴学派的机器证明研究一直居于国际领先地位的重要原 因。 机器证明的发展不仅要求进一步扩大机械化数学的领域，需要有更多的数学概念和 工具引入，在理论上深入发展，而且要求不断提高证明效率，在方法上有不断的创新。 微分几何曲面上曲线定理的机器证明 反过来，机器证明也能够推动一些新的数学概念和工具的产生，推动核心数学的发展。 应用c l i f f o r d 代数于几何定理机器证明的工作，正是产生于这个背景之下。 自1 9 9 4 年起，李浃波 2 4 2 9 第一个提出并应用c i i f f o r d 代数予几何定理机器证 明，结合吴方法创立了高效的几何计算和推理新方法，不仅使几何定理机器证明由经典 几何( 包括经典微分几何) 发展到现代几何( 包括现代微分几何) ，而且使更多的抽象数学 概念变为可以机器计算的，而且为机械化方法向现代理论数学和物理的其他领域的发展 起到桥梁作用，有重要的理论意义 在效率上，c l i f f o r d 代数方法“使证明过程往往变得极为简单，某些原来的方法所 感到难于处理的定理，也成为简易可行”( 吴文俊评论) 例如，平面几何中的五圆定理 是十分困难的定理，多次作为新定理被发现，用现有机器和纯粹代数方法还很难完成证 明我们用c 1 i f f o r d 代数方法则可以手算完成证明。机器证明的c l i f f o r d 代数方法同 样是几何研究的有力工具，它不仅能够很大程度地简化阻难定理的证明，而且能够解决 公开问题。例如二维射影几何中的e r d o s 猜想，曾被许多著名学者研究过。1 9 9 5 年李 洪波用c i i f f o r d 代数方法基本解决了这一问题 c l i f f o r d 代数对几何的表示具有以下特点： ( 1 ) 几何体有不依赖于坐标选取的符号表示，几何体之间的几何关系可以由符号间 的代数运算得到。 ( 2 ) 空间的等距变换，相似变换，共形变换等由生成元决定，生成元和变换结果都 可表为c l i f f o r d 代数中的元素。射影变换，仿射变换，多重线性变换等可用张量表示。 ( 3 ) 同一种几何常常有多种c l i f f o r d 代数可以表示，同一几何关系在同一种 c i i f f o r d 代数中一般有多种表示。 ( 4 ) 不同c i i f f o r d 代数之间的表示一般可互相转换，同一c l i f f o r d 代数内的不同 表示一般呈金字塔形，上层的抽象，下层的具体，一般只能自上而下地转换代数表示 几何定理机器证明的c l i f f o r d 代数方法的基本思想是结合作为推理机制、具有完 全性的吴方法和拥有高效的符号表示和计算功能的c l i f f o r d 代数。 证明一个由己知和结论部分组成的几何定理，一般有以下三个层次： 第一层次：在c i i f f o r d 向量代数表示下，对已知条件三角化，再对结论进行证明。 第二层次：在c i i f f o r d 几何参数表示下，对己知条件三角化，再对结论进行证明。 第三层次：在c l i f f o r d 代数表示或坐标表示下，对已知条件三角化，再对结论进行 证明。 大连理工大学硕士学位论文 对己知条件的三角化主要是基于c 1 i f f o r d 向量代数的向量方程组求解当无法得到 解时，引入部分几何参数表示，重新求解。在括号代数表示下，可选择的证明手段有双 二次终极多项式方法，直接收缩方法等等。在c 1 i f f o r d 向量代数表示下，可选择的证 明手段有重写方法，正则化方法，等等。在坐标表示下，可以采用吴方法，6 r o b n e r 基 方法，等等。 微分几何曲面上曲线定理的机器证明 2 预备知识及相关理论 微分几何学是数学的一个分支学科，它主要是以分析方法来研究空问( 微分流形) 的几何性质。古典的局部微分几何是研究三维欧式空间矿的曲线和曲面在一点邻近的 性质，它的发展和分析学的发展有着不可分割的联系。微分几何 3 4 起源于1 7 世纪发 现微积分之时，函数与函数的导数的概念实质上是等同于曲线与曲线的切线的斜率，函 数的积分在几何上贝i j 可解释为一曲线下的面积。当时，平面曲线、空间曲线及曲面的几 何也可作为微积分的应用来了解。 曲线是微分几何学研究的主要对象之一直观上，曲线可看成空间质点运动的轨迹 曲线更严格的定义是区间【口，6 1 到矿中的映射r ：【口川专矿有时候也把这映射的像称 为曲线。具体地说。设o 呵2 是欧式空间矿中的笛卡尔直角坐标系，r 为曲线c 上的点 的向径，于是有 r = r ( f ) = ( 川) ，) ，( f ) ：( f ) ) t 【口，6 】 上式称为曲线c 的参数方程，t 称为曲线c 的参数。 曲率度量了曲线上相邻两点的切矢量的夹角关于弧长的变化率，直线的曲率恒为 零，圆周的曲率等于其半径的倒数。挠率度量了曲线邻近两点的次法向量之间的夹角对 弧长的变化率，平面曲线是挠率恒为零的曲线，空间曲线如果不是落在一个平面上。则 称为挠曲线。具体地说，如果给定了两个连续函数“d 0 和f ( 曲，s e a ，b 】，则存在以 x ( s ) 和f ( s ) 分别为其曲率和挠率的曲线，并且这些曲线经过空间的一个运动可以互相叠 合。 2 1曲线论 我们对曲线作一些规定在直观上，e 3 中的一条曲线是指中的一点随时间t 的变 化而运动所得到的轨迹。换言之，矿中的一条曲线可以表示成从区间【口 川到的一个 连续映射： p ：【口 b 】- - h 驴 ( 2 1 ) 称为参数曲线。在矿中取定一个右手笛卡儿坐标系( d ；_ ，七 ，则曲线上的点 p ( r ) ( 口s f s 与向径石泌) 是等同的。命r ( f ) = 历( ，) ，则巾) 可以表示为 川) = 加) i + y ( f ) j + z ( f ) k ， ( 2 2 ) 大连理工大学硕士学位论文 因此，映射( 1 ) 等价于三个实函数川) ，j ，( f ) ，z ( ，) 。通常在固定的坐标系 d ；f ，j ，d 下， 把曲线记成 r ( f ) = ( f ) ) ，( f ) z ( f ”，t 【口，明， 0 ，口材 ( 2 1 1 ) 并且 r ( c r ) = a ，t ( f 1 ) = b ， 因此 i 塑剿= 医悟 亿埘 根据积分变量替换公式有 _ 螂d tl ，= 强，a l l 微分儿何曲面上曲线定理的机器证明 = 蜘砌卜 所以s 与参数变换( 2 1 1 ) 是无关的。 现在令 j ( f ) = i r ( t ) l d t ， ( 2 1 3 ) h i j s q ) 是曲线c 上从a 到t 的弧长由于j ( f ) 是f 的三次以上连续可微的函数，并且 掣：l 讲 o 出 由此得 出= l r v ) l a r ( 2 1 4 ) 凼是曲线的不变量，称为曲线的弧长元素。 2 1 2 曲线的曲率和f r e n e t 标架 设曲线c 的方程是r = r ( s ) 。其中s 是曲线的弧长参数。k s ) 是曲线c 的单位切向量 场。命 球( s ) = ( d ( 2 1 5 ) 命r = 忙( 叫，我们称r 为曲线r = r 在j 处的曲率，称西( d 为该曲线的曲率向量 i 劭 a o ) l = l ，口( $ ) 应( j ) = o ，所以曲率向量口( s ) 是曲线的法向量场。西( 曲有完全 确定的方向向量，将这个方向向量记作觑j ) ，称为曲线的主法向量。这样，曲率向量西( 可以表示为 d ( d = g o ( s ) ( 2 1 6 ) 由曲线的单位切向量场口( 曲和主法向量觑力，唯一地确定了曲线的第二个法向量 场 ，o ) = v t ( s ) 烈j ) ( 2 1 7 ) 称为曲线的次法向壁场，这样，在正则曲线上曲率r 0 的点有一个完全确定的右手单 位正交标架 r ( s ) ；口( 班烈j ) ，( j ) ，我们把它称为曲线在该点的f r e n e t 标架。在曲率 r o 的点，f r e n e t 标架 r d ) ；口( 珐反珐，( 曲 的三根轴分另h 称为曲线的切线、主法线和 次法线。 大连理工大学硕士学位论文 f 向我们叙述曲线的曲率和f r e n e t 标架的计算方法如果曲线r = r ( j ) 以弧长s 为 参数，则曲线的曲率及f r e n e t 标架可以根据定义直接算出。实际上， ) ：掣，r ：陋) l ：l i = ( s ) | ( 2 1 8 ) 珊 。 如果r 0 ，则 触。黼m m 溉) = 垫霰铲 ( 2 1 9 ) 如果曲线的方程是r = r ( f ) ，不是弧长参数，则 鲁= 俐， 所以 删= 尚川洲i ( f ) 对后一式再微分得到 川) = 掣圳w i ( f ) i 警i d s = 掣删w i ( f ) 1 2 删 所以，( t ) x r ( r ) = l r ( 0 1 3 砂( f ) 因此 = 仨j ；吾；丛，o ，= 毒 筹i ；磊畚， p ( t ) = r ( t ) x a 2 咩篙群 亿z 。， 2 1 3 挠率和f r e n e t 公式 因为，是单位向量场，故，上尹。此外，y = a x ，所以 9 = 矗x p + a x 声= 口x 毒， 这说明户上口。于是户必定与卢共线的，不妨设 户= 一矿( 2 2 1 ) 因此 f = 户声，( 2 2 2 ) 定义 r = 一户卢称为曲线的挠率。 微分几何曲面上曲线定理的机器证明 根据曲率、挠率以及f r e n e t 标架的定义，我们已经有 3 8 l ( s ) = 口( s ) 矗( s ) = r p ( s ) ( 2 2 3 ) 【户( s ) = - r p ( s ) 下面我们要求反s ) ，由于 r ( s ) ；口o ) ，以s ) 八s ) 构成空间矿的一个标架，所以向量 厦砖总可以表示成口，夕，的线性组合，不妨设 觑j ) = a a ( s ) + 6 风j ) + 钞( d 将上式分别与口，做内积，并利用标架向量口，卢，的单位正交性，我们 有 反。) = 一黝! ( s ) + ( j ) ( 2 2 4 ) 综合起来，我们便得到f r e n e t 标场 r o ) ；口