（系统分析与集成专业论文）基于数值计算的几何不等式自动生成和证明系统.pdf

摘要 几何定理的机器证明是自动推理和符号计算领域最为活跃的分支之一在几何定理机器证 明方法中，常用的有几何代数方法、演绎数据库方法和例证法等方法其中，数学机械化思想 的倡导者吴文俊院士提出的几何定理的代数证明方法，被认为是具有开创性意义的方法，带来 了几何定理机器证明的新发展近年来，随着计算机容量的扩大和计算速度的不断更新，计算 机在数学领域的应用也不断深入，另一种几何定理机器证明方法一定理机器证明的数值方法， 也得到了蓬勃发展在该领域，先后出现了数值并行法、例证法、单例试验法等多种用数值方 法对几何定理进行机器证明的方法，使得定理机器证明领域更得到了广阔的发展然而，上述 几何定理机器证明方法主要针对等式型定理的证明，不等式型定理的机器证明则一直是自动推 理领域中的一个难题 上世纪5 0 年代初，t a r s k i 发表了著名的初等代数与初等几何的判定问题，宣称在理 论上可以解决实几何问题，但由于其方法复杂度太高效率太低不能实现随后，c o l l i n s 提出了 柱面代数分析方法( c a d ) ，效率得到了提高，能证明一些稍难的几何不等式；吴方法出现盾， 有人将吴方法与l a g r a z l g e 乘子法结合，用求极值的方法处理一些有关不等式的几何问题，但 这些方法通用性和效率不理想1 9 9 8 年，杨路提出了基于胞腔分解的降维算法，这一算法能 有效处理含参根式，并最大限度地缩减维数。使不等式证明能达到较高的效率但是，这种降 维方法较多地利用了实代数系统方法，因而在实现时对符号计算软件有很大的依赖性，也比较 复杂 在已有定理机器证明数值方法的启发下，侯晓荣提出了一种新的几何不等式自动生成和 证明的方法，本文对该方法予以了具体的实现和测试，在该领域做了一次有意义的尝试我们 首先采用数值计算在例证法的基础上根据用户需求，猜测生成一些符合条件的几何不等式；然 后引入区间计算这一数值计算方法，以此作为计算工具，用作图的方法完成对指定不等式的证 明由于采用了数值计算，使得系统效率有很大的提高，同时甩区间计算的方法，也避免了计 算机进行单纯数值计算时丢失数值信息的弊端；而后用作图的方法，能够使证明过程脱离符号 计算软件和代数系统的束缚，达到简单明了的效果我们在w i n d o w s 平台上用v i s u a lc + + 编 程实现了该算法，达到了对方法有效性检验的目的，程序执行速度也表明其系统效率也是令人 满意的 关键词：几何不等式，自动证明，数值方法，区间计算，作图，生成 a b s t r a c t t h ea u t o m a t e dp r o v eo fg e o m e t r i ct h e o r e mi so n eo ft h em o s ta c t i v eb r a n c hi na u t o m a t e d r e a s o n i n ga n ds y m b o l i cc o m p u t a t i o nm e t h o d s ，i n c l u d i n gg e o m e t r i ca l g e b r a i cm e t h o d ，d e d n c t i v ed a t a b a s em e t h o da n dp a r a d i g m a t i cp r o v em e t h o dh a v eb e e n w i d e l ya p p l i e di l lt h eg e o m e t l i c t h e o r e mp r o v ef i e l di nr e c e n ty e a r s ，w i t ht h ee x p a n s i o no fc o m p u t e rc a p a b i l i t ya n du p d a t eo f i t sc o m p u t i n gs p e e d ，t h ea p p l i c a t i o no fc o m p u t e ri nm a t h e m a t i c a lf i e l dw a sd e e p e n e d a n o t h e r m e t h o d ，n a m e l yn u m e r i c a lm e t h o df o rt h e o r e mp r o v ew a sa l s ob e e ne x p a n d e dv i g o r o u s l ym a n v n u n l e r i c a lm e t h o d ss u c ha sn u m e r i c a lp a r a d i g m a t i cm e t h o d ，p a r a l l e ln u m e r i c a lm e t h o dw e r ep l e s e n t e d a l lt h o s eb r o u g h to u tg r e a tp r o g r e s si nt h e o r e ma u t o m a t i cp r o v e n e v e r t h e l e s s ，a l lt h o s e m e t h o d sw e r ea i m e da te q u a l i t yt h e o r e m sa n di n e q u a l i t yt h e o r e ms t i l lw a st h ed i f f i c u l tp r o b l e m i na u t o n l a t i er e a s o n i n gf i e l d i nt h e1 9 5 0 s t a r s k ip u b l i s h e dt h ef a m o u sa r t i c l ead e c i s i o nm e t h o df o re l e n l e n t a r ya l g e b r aa n dg e o m e t r y ，w h i c hd e c l a r e dt h a tr e a lg e o m e t r i cp r o b l e mc a nb er e s o l v e dt h e o r e t i c a l l y b u tt h i sm e t h o dc a nn o tb ei m p l e m e n t e dp r a c t i c a l l yt oh i g hc o m p l e x i t ya n dw a s p r o v e dt ob el n e f f i c i e n t l a t e r ，c o l l i n sb r o u g h tf o r w a r dt h ec y l i n d r i c a la l g e b r a i cd e c o m p o s i t i o n ( c a d lm e t h o d ， w h i c he n h a n c et h e e f f i c i e n c ya n dc a np r o v es o m e m o r e d i f l l c u l tg e o m e t r i ci n e q u a t i o n s t h e n ，a l o n g w i t h 胁m e t h o d am e t h o dc o m b i n i n g 胁m e t h o da n dl a a g r a n g em u l t i p o l a rh a sb e e np r e s e n t e d b u ta l lt h o s em e t h o d sw e r en o tg o o de n o u g hb e c a u s eo ft h el a c ko fg e n e r a lu s ea n de f b c i e n c yi n 1 9 9 8 、a na u t o m a t e di n e q u a l i t y - p r o v i n ga l g o r i t h mw a sp r e s e n t e db yy a n gl ub a s e do nam i x e d m e t h o di n c l u d i n gas o - e a l l e dc e l l d e c o m p o s i t i o n t h em e t h o dc a np r o v eo rd i s p r o v ep r o p o s i t i o ni n a ne x t e n s i v e ( ：l a s so f g e o m e t r i ca c i da l g e b r a i ci n e q u a l i t i e si n v o l v i n gr a d i c a l s h o w e v e rt h i sm e t h o d 出s od e p e n d so nr e a la l g e b r as y s t e ma n ds y m b o l i cc o m p u t a t i o ns o f t w a r ea n dm e a n w h i l ei sa1 i t d e b i tc o m p l i c a t e d i l l u n f i n e db ye x i s t e n tn u m e r i c a la u t o m a t e dt h e o r e mp r o v em e t h o d ，an m t h o d t op r o d u c ea n dp r o v eg e o m e t r i ci n e q u a t i o ni sp r e s e n t e di nt h i st h e s i s f i r s t l y a c c o r d i n gt ol h e u s e r sr e q u i r e m e n t w eu s en u m e r i c a lc o m p u t a t i o nt oe r e a t es o m eg e o m e t r i ci n e q u a t i o n sb a s e do n p a r a d i g m a t i cm e t h o d t h e n w ei n d u c tt h ei n t e r v a lc o m p u t a t i o na n dt a k ei ta st h ec o m p u t et o o l t 。h n p l e m e n tt h ep l o t t i n gf o rf u n c t i o n d e f i n e di m a g e b yt h ep l o t t e di m a g e s w ec e l lp r o v et h e g e o m e t r i ci n e q u a t i o n s t h em e t h o dh a st h r e em a j o ra d v a n t a g e s ：f i r s t l y , t h i sm e t h o di sb a s e do n n u n l e r i c a lc o m p u t a t i o n s ot h ee f f i c i e n c yw a se n h a n c e dg r e a t l y ；s e c o n d l y i tw o u l da v o i d1 0 s i n g m u c hn e c e s s a r yi n f o r m a t i o no fr e a ln u m b e r sb va d o p t i n gi n t e r v a lc o m p u t a t i o nw h e nt h ec o m p u t e r s t o r a g er e a ln u m b e r s ；t h i r d l y ，o w i n gt ot h ep l o t t i n gm e t h o d ，i tc a nd e v i a t ef r o mt h el i m i to fs y m b o l i cc o m p u t a t i o ns o f t w a r ea n da l g e b r a i cs y s t e ma n dc a np r e s e n tas i m p l er e s u l tw h i c hi sm o r e u n d e r s t a n d a b l et h em e t h o di si m p l e m e n t e db yav i s u a lc + + p r o g r a mn a m e d “c r e a t e ”w h i c h t e s t st h ev a l i d i t ya n de f f i c i e n to ft h i sm e t h o d k e y w o r d s ：g e o m e t r i ci n e q u a t i o n s ，a u t o m a t i cp r o v e ，n u m e r i cm e t h o d ，i n t e r v a le o m p u t a t i o n ， p l o t lc r e a t e 贺玲琳硕士学位论文答辩委员会成员名单 姓名 职称 单位备注 王席 学位论文独创性声明 本人所呈交的学位论文是我在导师的指导下进行的研究工作及 取得的研究成果。据我所知，除文中已经注明引用的内容外，本论文 不包含其他个人已经发表或撰写过的研究成果。对本文的研究做出重 要贡献的个人和集体，均已在文中作了明确说明并表示谢意。 作者签名：塑盥日期：丝竺：生：塑 学位论文授权使用声明 本人完全了解华东师范大学有关保留、使用学位论文的规定，学 校有权保留学位论文井向国家主管部门或其指定机构送交论文的电 子版和纸质版有权将学位论文用于非赢利目的的少量复制并允许论 文进入学校圈书馆效查阙有权将学位论文的内容编入有关数据库进 行检索。有权将学位论文的标题和摘要汇编出版。保密的学位论文在 懈密后适用本规定 学位论文作者签名：该泠搦 日期：趟：鱼：逸 导师獭：籼、l c 日期：礁【：堡兰 第一章绪论 数学机械化和公理化是数学诞生以来就并有的两大数学思想方法，电子计算机的诞生和使 用促进了机械化流派的发展和复兴当前数学机械化的核心内容是实现用计算机对数学定理的 发现、整理和证明而其中尤以几何定理的机器证明为近年来数学机械化领域的热点，也取得 了重大的突破和发展 1 1定理机器证明的历史 所谓数学定理的机械化证明即把某一类定理当作一个整体加以考虑，建立一种统一 的、确定的证明程序，使得该类中的每个定理，只要按此程序机械地( 刻板地) ，按部就班地 一步一步实施下去，经有限步之后即可从数学命题的假设推断出数学命题的结论在若干附加条 件之下是否为真，命题为真时即为定理对一类定理而言，这种统一的确定的证明方法称为定 理证明的机械化方法依照机械化方法实施数学定理的证明称为数学定理的机械化证明建立 和提供数学定理机械化方法的数学原理称为数学定理证明的机械化证明原理实现数学定理证 明的机械化，是数学科学发展的一次飞跃但是，对这一领域的研究可追溯到古代 从问题出发，建立算法的机城化是中国古代数学的突出特点成书于汉代的九章算术 就是算法机械化的典范，书中把数学问题分成方田、勾股、方程等九大类，对每一类问题给出 解题的方法 以希腊几何学为代表的古代西方数学研究的中心问题不是问题的分类求饵，而是在建立公 理体系的基础上一个一个地证明各式各样的几何命题；但在几何命题机器证明这条道路上，历 史上些大师级的数学家也曾进行过艰辛的探索吼 1 7 世纪，法国数学家d e s c a r t e s 发明了坐标方法，创立了解析几何，使初等几何问题代数 化，在世界上第一次把无章可循的几何证明题纳入了有一定规范形式的代数框架，为后来的几 何定理机器证明打下了基础后来，德国数学家l e i b n i z 也曾提出过“推理机器”的设想，可 看作机械化思想的初步尝试 然而，第一次真正提出对某一类几何命题假设的机械化检验方法的是大数学家h i l b e r t 1 8 9 9 年，他出版了著名的几何基础，书中给出了欧儿里得几何的一个完备的公理系统，该 书被看成是第一部论述数学公理化的专著 定理证明的重要进展是属于t a x s k i 的1 9 5 0 年，他推广了关于代数方程实根数目的s t u r m 法则，由此证明了一条引人注目的定理：“一切初等几何和初等代数范围的命题，都可以用机械 方法判定”t a s k i 也确实提出了一套能判定任一个初等几何或初等代数命题的机械化方法可 是这方法的计算复杂度太大了，即使用快速的计算机，也不能在合理的时间内( 比如说几小时 或几天) 证明稍难的几何定理后来，有人改进了t a s k i 的方法并在计算机上实现，效果仍不 理想但即便如此，由t 缸k i 的工作导致的进展加强了人们在数学机械化道路上前进的信心， 开拓了用代数方法进行机器定理证明的研究方向 1 9 5 8 1 9 6 0 年i _ ，j ，数理逻辑学家壬涪设计了兰个程序，用计算机证明了b aw r n s s e l i 和 a n w h i t e h e a d 的名著数学原理中的几百条有关命题和一阶逻辑的定理，仅用了9 分钟 就在同一对间a n e w e l l 和h a s i m o n 也傲了类似的工作1 9 7 6 年，美国豹两位年轻的数学家 在高速电子计算机上，用1 2 0 0 小时的计算时间，证明了著名的四色定理，使数学家们1 0 0 多 年来未能解决的这个难题得到了肯定的回答这些工作极大地推动了定理机器证明研究的深入 发疆 然而，人们期待的是能把初等几何定理成批地证出来但自t a t - s k i 的定理发表后的2 0 多 年中，初等几何定理的机器证明并未取得人们预期前进展及至中国数学家的加入，几何定理 机器证明的研究才取得了迅猛的发展 1 2 等式型定理祝器证明的现状 7 0 年代后期以来，几何定理机器证明取得了突飞猛进豹发展，目前已形成了代数方法、几 何基方法、搜索方法等三类行之有效的方法吼 代数方法 正当人们在一簿奠展之际，我国数学家在定理机器证明领域揭开了崭新的一页吴文俊在 中国青代数学机械化与代数化恩想的启发之下，独辟蹊径，提出了自己的机械化方法这一证 明几何定理的新方法已被广泛称为吴方法它不仅可以在微机上有效遣证明许多已知定理，还 能用来发现新的不平凡的几何定理吴方法的成功引起了自动推理界的普遍关注，并受到了国 内外专家学者的高度推崇，也带来了过去2 0 多年几何定理机器证明的发展和繁荣，被公认为 是机器证明领域的里程碑式的突破吴方法的关键是把几何命题化成代数形式加以处理，因此 也称为代数方法 代数方法进行几何定理机器证明 4 1 的第一步是把几何问题代数化，建立坐标系，并为命题 涉及的几何图形的点选取适当的坐标，然后把命题的条件和结论表示为坐标的多项式方程组， 检查条锌方程组的解是否满足结论方程组通常的凡何命题涉及的多项式方程组都是非线性 的，一般无法将约束变元求出吴方法是利用伪除法判定条件方程组的解是否是结论方程组的 解，而且利用吴方法不仅可以判断定理的正确与否，还可以自动找出定理赖以成立的非退化条 侔，这是传统的方法无法傲到的多项式的伪余除法可以用符号演算的方法在计算机中实现 在吴方法的影响下，相继出现了许多新的方法，如数值并行法、例证法、概率法等其他代 数方法，所有这些方法都能有效地判定等式垄的初等几何命题，班及球面几何、菲欧几何韵命 题 几何量方法 2 尽管吴方法带来了几何定理机器证明突飞猛进的发展，但以吴方法为代表的代数方法在证 明几何定理的过程中要用到多项式的运算。由于这些多项式少则几十个，多达成百上千个，并 不能让人们在合理的时间内看明白因此，给出几何命题的让人能读懂的可读证明的问题在多 次机器证明的国际学术会议上被许多专家提了出来 宴际上从6 0 年代开始，欧美的一些科学家已开始初等几何定理的可读性证明研究，但 一一直未取得实质的突破性成果直至1 9 9 2 年，张景中以其多年研究的面积法作为基础，提出消 点算法，用于对付可读证明这个3 0 多年进展甚少的难题结果大见成效随后，在张景中、周 成青、高小山的合作努力下，消点算法日趋完善并编程得到了实现，在n e x t 微机上产生了r 1 7 8 条非平凡的几何定理的可读证明，从而在几何定理可读机器证明方面取得了突破性的进展这 项工作被自动推理领域的国际同行誉为“计算机发展几何问题解题能力遭路上的里程裤”，4 自 动推理领域3 0 年来最重要的工作” 消点法包括一组作图规则，一组几何量和关于这些规则和几何量的一组消点公式该方法 的基本思想是：利用构图规则将欲证几何命题中涉及的图形构造出来，并在构图的过程中生成 关于点的约束条件，同时将欲求证的命题表示成图中几何量的等式形式，然后利用消点公式， 接照点在作图时出现的相反顺序，依次从结论等式中消去，最终结论等式会化为显然成立的等 式 后来，杨路等1 5 i 又将消点法推广到非欧几何，成功的证明和发现丁大量的新的非欧几何 定理李洪波、王东明发展了不变量方法，把消点法推广到了广义的向量空间，即c l i f f o r d 代 数 搜索方法 以面积法为代表的几何量方法，尽管能给出一大类几何定理的通用的证明方法，并产生可 读证明，但其证明的过程不能完全合乎人们通常的思维习惯因此，我们希望计算机能像普通 的人证明几何定理时那样去证明，产生人们通常给出的那种方式的证明 实际上这样的想法在机器证明研究初期就有1 9 6 0 年，h g e l e r n t e r ，j r h a n s o n 和 d w l o v e l a n d 联合发表的篇文章【4 】中提出了从结论出发进行搜索的后推链方法到了1 9 7 5 年，a j n e v i n s 又提出了前推链方法，但是仍不能实现为有效的算法和程序随后的几十年 里，科学家基于这两种推理设想进行了大量的探索，但始终收效不大直到1 9 9 6 年，张景中、高 小山、周成青提出了一个基于前推模式的“几何信息搜索系统”或“几何推理数据库”( g i s s 或g d d ) ，成功的证明了1 6 1 个非平凡的几何命题，收到了良好的效果这种搜索方法的思 想就是根据几何命题所给的条件、已知的公理定理及公式等推理规则，通过大量的试验匹配 的方法生成一个几何性质的数据库，近而检查要证明的结论是否在该几何库中，以达到证明的 效果 3 1 3 不等式型定理机器证明的现状 上述2 0 多年来所获得的进展主要局限于等式型几何定理的证明，而对j 二不等式型定理的 机器证明的研究则举步维艰主要原因在于其相关算法本质上依赖实代数与实几何，其计算复 杂度会随着维数( 参数的个数) 的增加而快速增长从算法的角度看，除了节约内存消耗，效 率的改进也是非常有意义的，当要求成批地验证非平凡的命题时，一个低效的算法是不能在人 们所能忍受的时间内解决问题的 所谓一个几何定理是等式型的是指将几何命题引入坐标系后，定理的条件和待证的结论都 可以化为左右两个多项式相等的形式 3 1 而不等式型定理，一般都是用半代数系统来描述的， 即定理的假设部分是由多项式等式或不等式来表达，而结论部分包含多项式不等式的定理 1 9 8 5 年，吴文俊在上海召开的一次学术会议上就指出：不等式的机器证明是“一大难题”， 十余年来没有取得重大进展吼由c o l l i n s 提出盾又经他人改进的“柱形代数剖分”算法( 简 称c a d ) ，已经能够在计算机上判定一些难度不大的代数与几何的非等式型命题后来，周咸 青、高小山等将c a d 原有算法和吴方法结合，在这方面做了有益的探讨，可以处理原先不能 处理的一些问题但与等式型定理机器证明研究进展的现状相比，这些方法的通用性和效率还 很不理想，距离成批、成类判断命题真伪的目标还相距甚远 不等式证明机械化的困难之一，在于实代数的一个最基本的问题长期没有解决，这就是 多项式的判别系统问题根据实系数一元二次方程的判别式是正是负还是零，可以断定它有没 有实根，两个实根是否相同这是代数学的经典结果，也是中学数学课程的重要内容对高于 二次的多项式，情形更为复杂，要用一组不等式或等式才能说清楚根的情况这样的一组等式 或不等式，如果有的话，就叫做该多项式的判别系统但是，为什么说不等式的机器证明与判 定系统密切相关呢? 因为即使最简单的不等式问题，也可能涉及判定系统例如，要问不等式 一+ o 一+ b x 2 + c z 一9 0 在a ，b ，c 满足什么条件时对一切实数z 成立，就等价于问这个5 次 多项式何时无实根这正式判定系统所要回答的问题之一 1 6 世纪，数学家发现了3 次和4 次方程的求根公式在此基础上，建立了实系数3 次和 4 次方程的判别系统顺便提一句，实系数4 次方程的完全判别系统，是2 0 世纪6 0 年代才 建立起来的5 次或更高次的多项式，就没有求根公式了有没有判别系统? 如何找寻它的 判别系统? 这是实代数领域长期未能解决的一个基本问题这个问题不解决，大量的几何不等 式问题，代数不等式问题，以及许多科技领域与不等式有关的问题就无法从一般的推理角度来 解决大家熟知的s t u r m 法则，处理的是数值系数代数方程的实根问题，而在一般的推理过 程中，往往要问系数满足什么条件时有实根，这就需要对代数方程建立判别式系统方程的次 数越高，判别式系统就越复杂特别是，5 次和更高次的方程没有求根公式，这使问题更难下 手直到1 9 9 5 年，4 次方程的判别式系统已经建立3 0 多年了，关于实系数5 次代数方程根的 完全分类的显示判定问题，即判别式系统问题还未解决 计算机自动推理促进了这一古典课题的研究1 9 9 6 年，杨路、侯晓荣和曾振柄提出了对 任意次的实系数代数方程建立完全判别系统的通用算法，使这个实代数的基本问题得到了完满 4 的回答，为实代数的自动推理提供了有效的工具用他们提供的m a p l e 程序，在微机上很容 易求出直到8 次的代数方程的判别系统同时，依据多项式完全判定系统的理论编制的程序 i n v e n t o r 和d i s c o v e r e r 具有发现不等式的功能 代数方程判定系统的研究进展为不等式机器证明的研究提供了基础但是，几何不等 式机器证明的研究仍要克服它本身固有的困难不等式机器证明的困难除了依赖于实代数的自 动推理外，还因为其复杂度随维数增加而急速升高例如前面提到的c a d 算法去做代数剖分 就非常困难，随着参数空间维数的增加其计算复杂度增加很快当命题的假设中含有若干代数 方程时，一个自然的想法是消去一些变元以降低维数而这样做所遭遇的新的困难是，必须有 效地处理带参数的根式国内外常用的办法是引进新的变元和方程，这使问题的维数升高而复 杂化，常常超出计算机的能力 1 9 9 8 年，杨路发表的一篇论文j 中提出了不等式机器证明的基于胞腔分解的降维算法， 这一算法能有效处理含参根式，并最大限度地缩减维数，使不等式证明达到较高的效率根据 以上算法，杨路用m a p l e 语言编制成的通用程序b o t t e m a 已在p c 机上成功地验证了1 0 0 0 多个不等式，其中近半数是近期提出未加证实的猜想，运用该软件已能成批验证非平凡的不等 式，就两个自由度的情形，其效率与等式型几何定理证明软件相比已不相上下这使得不等式 机器证明这一难题得到了突破性的发展 1 4 本文的工作 目前，几何定理机器证明的研究已经取得了突破性的进展，不等式型定理证明也取得了 定的成果不仅提出了多种有效的方法，还成功的开发了一些定理证明的智能系统，其中一些 成果已经被应用到几何教育领域中去 但是目前的方法和系统大多侧重于定理的严格证明，即使是杨路提出的基于胞腔分解的降 维算法也由于较多地利用了实代数系统方法，因此要很大程度上依赖符号计算软件来实现此 外，如何进一步提高证明的效率，提出一些有特色的证明方法，发现一些新的不等式定理等方 面现有的方法仍有一些需要探索和改进的地方 针对上述问题，侯晓荣提出了一种基于数值计算的不等式自动证明的新方法本文依据该 思想，在数值计算方法基础上实现了不等式的自动生成和证明该方法是对数值方法的一个推 广，充分利用了数值方法效率高的特点，可以在很短的时间内实现对指定几何关系的不等式的 生成，并且引进区间计算为作图工具的方法对得到的不等式进行进一步的证明该方法中，我 们利用数值计算代替符号计算能大大降低系统资源的要求，同时能加快生成不等式的速度基 于该搜索方法，我们用非符号计算语言v c + + 设计编写了几何不等式自动生成和证明系统 测试系统不仅实现了对几何不等式的自动生成，并且用作图的方法实现了严格地进行了不等式 的证明，具有效率高，证明清晰等特点，充分验证了这种方法的有效性 5 第二章几何定理证明的数值方法 数值计算方法，又称为数值分析，是利用计算机进行科学计算的主要方法随着计算机的 发展与普及，继试验方法、理论方法之后，科学计算已成为科学实践的第三种手段，求解各种 数学问题的数值方法已被广泛应用于不仅是自然科学，还包括生命科学、经济科学和社会科学 等各领域 2 1 几种数值方法 数值计算方法是以数学问题为研究对象的，它不象纯数学那样只研究数学本身的理论，而 着重研究求解的数值计算方法及与此相关的理论，包括方法的收敛性、稳定性及误差分析，还 要根据计算机特点研究计算时间最省的计算方法因此，数值计算的任务就是提供在计算机上 实际可行的、理论可靠的、计算复杂性好的各种数值方法下面是数值计算方法的几种基本解 题思想【8 】一【1 2 ： 1 “构造性”方法 数值方法中许多问题的存在性证明以“构造性”方法为基础所谓用“构造性”方法证明 一个问题的存在性，是指具体地把这个问题的计算公式构造出来，这种方法不但证明了问题的 存在性，而且有了具体的计算公式，便于编制程序上机计算 我们厢一个简单的例子说明这个特点 例2 1 构造性证明：实系数二次方程z 2 + 2 b x + e = 0 ，当b 2 c 时，有两个实根 证明： 对任意z ，b 和c ，有 z 2 + 2 b x + c = z 2 + 2 b x + b 2 一b 2 + c = ( x + b ) 2 + c b 2 因此，当且仅当 ( + 酏2 + c b 2 = 0 时，o 是它的根，亦即 ( $ + b ) 2 = 矿一c 将两端开方并注意5 2 一c 0 ，可以推出当且仅当 。+ b = 士厶2 一c 6 时，z 是根，从而 方法 z = - b 土6 2 一c 这样就用求出两个根的构造性方法证明了方程存在两个实根，显然也得到了两个根的计算 2 “离散化”方法 把求连续变量问题转化为求离散变量问题，称为离散化 一个连续的数学问题要上机计算，必须进行离散化离散化可以认为是数值计算中最基本 的概念和方法之一例如把定积分离散成求和。把微分方程离散成差分方程等等 3 “递推化”方法 所谓递推化，其基本思想就是将一个复杂的计算过程归结为简单过程的多次重复由1 二递 推化算法便于编写计算机程序，所以数值计算中许多数值方法常常采用递推化方法 例22 对给定的o ，计算多项式 的值 只l ( z ) = n n z “+ a - 1 z “一1 + + n l z + n n 解：可利用递推公式 ：芝一，。+ 。一。 c z ， 对= 1 ，2 ，n 反复执行( 2 1 ) 式，最终得到的就是多项是r ( z ) 的值 4 “近似替代”方法 计算机运算必须在有限次后停止，所以数值方法常表现为一个无穷过程的截断，把一个无 限过程的数学问题，转化为满足一定误差要求的有限步来近似替代 2 2 数值计算中的误差 采用数值方法求解数学问题给出的解答仅仅是所要求的真解的某种近似，因此研究数值方 法，必须注重误差分析，分析误差的来源，误差的传播情况以及对计算结果给出合理的误差估 计 误差的来源多种多样，但大多可归为如下的三类m 【9 】 1 模型误差 用计算机解决科学计算问题首先要建立数学模型，它是对被描述的实际问题进行抽象、简 化得到的用不同的数学语言描述、刻画问题时，对应不同的数学模型，此模型与原工程问题， 7 总是有差异的，这种差异称为模型误差建模的关键问题是如何选择恰当的数学语言去刻画淡 盯j 题，使其模型误差最小若模型误差超出了允许范围，采用任何方法求解此数学模型都将失 去任何实用价值要真正定性特别是定量分析模型误差范围是很困难的，有待于在实际中，针 对问题去摸索相应的方法 2 观测误差 在数学模型中总包含有一些观测数据，如温度，长度，电压等等，这些数据的值一般是由 观测或实验得到的，由于观测不可能绝对准确，由此产生的误差称为观测误差 3 方法误差( 也称为截断误差) 同一数学问题，采用不同数值方法，有不同的误差称为方法误差例如对同一积分，采用 矩阵公式、梯形公式、抛物线等数值积分公式，误差明显不一样弼时，在数学模型不能得到准 确解时，通常要用数值方法求它的近似解，例如常把无限的计算过程用有限的计算过程代替， 这种模型的准确解和数值方法的准确解之阔的误差称为截断误差 4 畲人误差 当算法给定时，要实现算法，就要对数进行四则运算在计算机中，存放一个数只能是有 n j j - 。一 限位数，在计算过程中，必须进行舍入，倒如1 0 3 圭3 3 毫大量的计算必带来舍入误差 的积累和传播 上述几种误差都会影响计算结果的准确性，数值计算中除了研究求解数学问题的数值方法 外，还要研究计算结果的误差是否满足精度要求，这就是误差估计问题但前两种往往很难独 立完成，数值计算中用不到描述自然现象，也用不到观测误差，而主要研究的是方法误差和舍 入误差对计算结果的影响 2 3 定理证明的数值方法 几何定理机器证明的数值方法有时也被归类为代数方法但数值方法不涉及通常代数方法 进行的符号演算，只进行数值计算，主要包括单点例证法和数值并行法 定理机器证明的数值方法的出现被认为是一个具有深刻哲学意味的发展一直以来，人们 关于归纳和演绎争论都喋喋不体一方面，人们往往受传统观念的束缚，认为“举例子做试验 完全不能算是证明”，只有严密的推理和演绎才是可靠的证明而另一方面，人类认识自然的 一个基本方式就是从个别到一般，从具体到抽象的经验归纳法从古到今，有许许多多的数学 定理是通过列举大量、具体的实例做实验，通过归纳发现的这种发现与证明的矛盾深深地困 惑着人们哲学家j s m i l l 对此也深感困惑：“为什么在有些场合，单个实例对完全归纳法是 足够的，而在别的场合，大量的并发的实倒( 已知或推测没有任何单一的例外) 在确定一一个全 称命题方面却进展不大呢? ”而在几何定理机器证明领域，正当吴方法取得举世瞩目的成功 的时候，另一个有趣的方法出现了 8 1 9 8 6 年，洪加威发表在中国科学上的文章能用例证法来证明几何定理吗? 中提 出了著名的例证法 】，大体思想是：对于一类平面几何定理，只要按照一个简单的规则去举 例子，并且对这个具体的数值例子的计算( 或作图) 到一定的精确程度，就完全可以用来精确 的判定一个一般的几何命题后来，王东明澄清了洪加威方法中的不可约问题，并对h i l b e r t 交点型定理分析了计算复杂性，给出了代数簇包含关系的例证法例证法的原理适用干更广阔 的范围，但洪加威所设想的算法复杂度太高，迄今未能在计算机上有效地实现 后来，张景中和扬路叉提出数值并行法【曲】，形式上更接近归纳法其基本的含义是：具有 某种一般性的大量实例可以证明一个一般的几何命题其设计思想是用数值计算代替符号计算 以减小内存消耗；用并行处理取代串行处理以缩短运行时间这是第一个具有实践意义的数值 方法，据此编制的“l 类几何定理证明器”已经受了实践的检验，可以在很短的实践内证明颇 不平凡的定理 近年来又出现了一种效率较高实用性较广的数值方法，叫做单点例证法 1 ( j l 该方法第一 次表明在一定意义下不准确的浮点运算可以用来作严格的推理，具有试验的性质，因而真正全 面地实现了例证法的美妙设想， 下面我们就分别介绍上述后两种方法的原理，并用实例来对其进行说明 2 3 1 数值并行法 简单的讲，数值并行法就是用一组例子来解决某些数学问题的方法例如证明下面的等式 是一个代数恒等式 ( z + 1 ) ( z 一1 ) = z 2 1( 22 ) 如果将等式左边直接展开移项，很容易就可以证明但也可以用数值实验的方法证明取z = o ， 两端都是一1 1 取x = 1 ，两端都是o ；取z = 2 ，两端都是3 这就证明了上式是恒等式因为我 们知道，一元二次方程至多有两个根现在有三个数都使它成立，这就表明它是恒等式这只 是一个简单的例子，那么是否对于一般的代数恒等式都可以类似的证明呢? 通过下面一些引理 和定理的介绍来回答这一问题1 3 ， 4 1 命题2 1 设f ( z ) 和g ( z ) 都是不超过n 次的多项式如果有n + 1 个不同的数a o ，a l ，a 。 使得f ( a k ) = g ( 。 ) ，( = 0 ，1 ，n ) ，那么等式 f ( x ) = g ( z ) ( 2 3 ) 是恒等式 证明；令日( z ) = p ( x ) 一g ( z ) ，则h ( x ) = 6 为次数不高于n 次的一元代数方程已知有 n + 1 个不同的数0 1 ，a 2 ，o 。使得f ( a k ) = a ( a k ) ，( = 0 ，1 ，n ) ，可得f ( x ) = 0 有n + 1 个 不同的根；而一元n 次代数方程至多有n 个根；因此日( z ) = o 是零多项式i 即f ( x ) = g ( 。) 是恒等式 命髓22 殴f ( x l ，z 。) 是。l ，z 。的多项式，它关于。* 的次数不大于”对= 9 l ，2 ，m ，取数组( 女，j ) 0 = 0 1 ，2 ，n ) ，使得j j 时a ( k ，j ) a ( k ，j ) 如果对任一组 ( j l 、，2 ，) ，都有f ( a ( 1 ，j 1 ) ，n ( 2 ，j 。) ，a ( m ，m ) ) = 0 ，那么多项式f ( x l ，z 。) 足恒为零 的多项式， 由上面两个命题可以发现，对于一个一般的代数恒等式都可以利用这种方法举例子证明 一般地，在命题232 的条件下，需要验算( n 1 + 1 ) ( 7 比十1 ) ( n + 1 ) 组例子，可以按照下面 几步完成 6 】： 首先要估计f ( x 一 ，。) 关于各个变元的次数的界多项式f ( x ，。) 通常是没经过 整理的如果整理好了，就马上可以看出是不是恒等j 二零，也不需要证明了，既然没整理，代 数式关于各个变元的次数也不是直接看出来的，要一些方法进行变元次数的估计 接下来是确定用哪些数值代入检验假设已估计好了z 的次数不超过n ，那就让z 这个变元取n k + 1 个不同值，这” + 1 个不同的值a ( k ，o ) ，n ( ，1 ) ，( ，n k ) 组成有限集 4 k ( k = 1 ，2 ，m ) 从且l ，a 2 ，a 。中各取一个：从a l 中取1 的一个值，从a 2 中取0 2 的一个值，从4 。中取z 。的一个值，这样凑出( x ，z ，。) 的值又血中有n t + 1 个数， 所以共可以找出( n 。+ 1 ) ( n 2 + 1 ) ( n + 1 ) 个数组来，这些数组构成的集合，叫做规模为 ( ”1 + 1 ) ( n 2 + 1 )( n k + 1 ) 的“格阵” 最后，将格阵中的每组值都代入f ( z t ，z 。) 加以检验，若有一组值使f 0 ，那就找 到了一个反例说明不会有f 恒为零，不用再检验下去了若每一组都使f = 0 ，便证明了f 恒 等于零比如耍验证等式( 。+ ”) 0 y ) = z 2 一y 2 是不是恒等式，首先看出它是关于变元扎y 的次数不超过2 ，故要在( 2 + 1 ) ( 2 + 1 ) = 3 + 3 的格阵上检验让x 在( 0 ，1 ，2 ) 中取值，y 也在 ( 0 ，1 ，2 ) 中取值，得到格阵中的9 组值：( 0 ，o ) ，( 0 ，1 ) ，( 0 ，2 ) ，( 1 ，o ) ，( 1 ，1 ) ，( 1 ，2 ) ，( 2 ，o ) ，( 2 ，1 ) ，( 2 ，2 ) 分别代入检验即可 上面介绍了数值并行法证明代数恒等式的基本原理，如果能把几何问题化为代数恒等式的 检验或代数式的计算问题。便也能用举例的方法实现对于一般的几何命题，机器证明主要是 按照下面三个步骤进行： ( 1 ) 从几何公理系统出发，引进代数系统与坐标系统，使得几何命题代数化 ( 2 ) 将几何命题假设部分的代数关系进行整理，然后按照确定步骤验证命题结论部分的代 数关系式能否从假设部分已整理成序的代数关系式中推出 ( 3 ) 依据( 2 ) 中的确定步骤编程，并在计算机上实施，以得出命题是否成立的最后结论 由于计算机只能识别有限的事物，因此步骤( 2 ) 中的代数关系式必须以有限的形式出现