初等几何定理机器证明的基本原理

1976与1977之交,我发现了一个初等几何定理证明的机械化方法,见文献[4].这一方法适用于各种无序的但满足 Pascal 公理的初等几何,或各种初等几何中不牵涉次序关系的那类定理.本文§4叙述了这一方法所依据的基本原理并给出了详细证明.在§2与§3中则阐述了基本原理所依赖的关于多项式组的整序理论与代数簇的构造性理论.二者俱源出 Ritt 的著作,见文献[2,3].最后在§5中以 Morley 定理与我所发现的Pascal 锥线定理为例,说明这一方法在计算机上实施的具体情况.     

初等微分几何的机械化证明

本文系文献[1]关于初等几何机械化证明的继续,文中指出,应用同样的原理可给出一个算法,足以判定初等微分几何中一个适当的叙述是否是一真实的定理,方法是依据Riquier-Ritt-Thomas的理论^[2,3],这些理论本身就是算法性的。     

几何学机械化方法Ⅰ.初等几何

依据多项式组的 Rilt 原理以及0点分解定理, (见[R 1,2]与[WU 4,5]),作者提出了几何学的一种机械化方法。除应用于解高次联立代数方程组外。本文以初等几何为限,指出如何依据这一机械化方法以建立构造性的代数几何学,以及如何应用于几何定理的机器证明与机器发明。在下一文中,将推广这一机械化方法于微分几何。     

三角恒等式与初等几何定理的机械化证明

一、三角恒等式的机械化证明我们知道,适当选取模型,双曲几何、椭圆几何中的定理证明几乎可以全部化为三角函数与双曲函数的运算。即使在欧氏平面几何中,三角函数的应用有时也会使证明大大简化。但三角函数的运算往往是既繁琐又要很高的技巧,特别是当涉及的几何问题复杂时手算几乎是不可能的。吴文俊在文献[4,6]中指出,可以利用三角函数满足的代数关系及 Ritt-吴文俊原理机械化地证明三角函数公式。本文将给出更直接的方法,并用之于几何定理的证明。当定理涉及角度及方向时,该方法特别有效。     

一种几何定理机器证明的零维化方法

本文对一类初等几何定理的证明给出了一种机械化方法，利用这种方法，可计算出一个由有限个素理想组成的集合，所有属于假设部分对应的某一扩域上的理想的素理想都在这个集合中出现并且可以挑选出来．因而一个几何定理一般真确，当且仅当终结多项式属于全部的这种素理想，即对其不可约特征列的余式为零．     

构造型几何定理及其机器证明系统

Hilbert 机械化定理表明,Pascal 几何中构造型交点定理可以机器证明。1982年,吴文俊教授给出了机械化定理的构造性证法。本文指出,通过添加若干新的构造类型,有更广泛的一类平面几何定理,其机器证明可以按照同样的构造性证法实现,我们称这类定理为构造型几何定理。作者适当调整吴文俊算法的步骤,在 HP1000小型计算机上建立了构造型几何定理的机器证明系统,效率大大提高,从而成功地证明了许多不平凡的几何定理,并且独立发现了相当深入的结果。     

一道射影几何名题的思考与探索

<正>文[1]给出了一道几何题的8种初等证法,其中,证法1是文[2]中华罗庚先生给出的简洁证明,证法2是文[3]中利用共边定理给出的更加简洁的证明.下面来探讨一下这个有趣的几何题.例1在四边形ABCD中,设K=AD×BC,L=AB×CD,M=AC×BD.     

连分数与类数及其他

本文用连分数给出虚二次域的类数公式,见文中的定理4.结合Hirzebruch和zagier的结果(定理5),就完全了用连分数给出虚二次域的类数公式的结果.另外还讨论了一类虚二次域类数的可除性,即有 定理6.设l,q均为正整数,且q≥2.如0>△=1-4q^l为无平方因子整数,则l除尽虚二次域(Q(△^1/2)的类数. 文献[6]中,用了代数几何方法证明了当l为奇素数时的情形,本文只用初等方法.最后,文中给出了一个实二次域类数的初等公式.     

蝴蝶定理及其推广

蝴蝶定理是初等几何中的近代名题，可称为数学殿堂里的一颗璀璨的珍珠．自1985年杜锡录教授介绍到我国以来，不少数学家、数学教育工作者对此作过研究．本文在给出蝴蝶定理的一个简洁证明的基础上研究其推广形式并加以证明．     

关于仑巴菲特引理的证明

１８４０年莱莫斯（ｌｅｍｅｓ）提出命题：“两内角平分线相等的三角形是等腰三角形．”很难用纯几何方法证明．瑞士几何学家斯坦纳（ｓｔｅｉｎｅｒ）第一个给出了证明,于是该命题就成了著名的“斯坦纳──莱莫斯”定理,但证法比较麻烦．于是人们又寻求定理的简单证法,大约于１９４０年前后,有人基于法国数学家仑巴菲特（Ｒｅｂａｆｆｅｔ）的引理“三角形中大角的平分线小些．”利用反证法,给出了一个较简单的证法,但美中不足的是引理的证法,如同定理的证法一样困难;如朱德祥先生在《初等几何研究》（高等教育出版社,１９８５年…     

二项式定理的概率论证法

应用广泛的二项式定理除了可用数学归纳法证明外,还可用组合分析或数学分析等方法分别证明之。本文给出一个完全只用初等概率论的知识的方法来证明二项式定理。 定理:设a,b里任意实数,n是正整数,     

Mazur-Orlicz定理的一个初等证明

在文献[1]中，作为矩阵求和法的一个重要定理——Mazur—Orlicz定理，其证明是借助于许多工具与手段给出的，十分繁琐。现用初等方法给出一个简化而直接的证明。     

Farkas定理的新证法

本文用初等方法对著名的Farkas定理给出新的证明,避免了原有艰涩的证明过程,论述简单明了。     

D ickson定理和H all定理的初等证明及二定理的等价性

论证了二定理的等价性,给出了H a ll定理的初等证明,展示出求得H a ll方程解的个数的可操作性.再利用二定理的等价性,又给出D ickson定理的初等证明.对求解D ickson方程解的个数,也有鲜明的可操作性.     

几何不等式的一个新证明

本文用初等微积分方法,对几何不等式给出一个新的证明。     

椭圆一个定理的又一初等证明

定理　椭圆Ｃ：ｘ２ａ２＋ｙ２ｂ２＝１（ａ＞ｂ＞０）有且仅有两条对称轴：直线ｘ＝０和ｙ＝０．文［１］指出,这个定理的证明一般要用到仿射几何知识,同时文［１］给出了一个初等证明．笔者再给出这个定理的又一种初等证明如下．定理的证明　易验证直线ｘ＝０和ｙ＝０均是椭圆Ｃ的对称轴．因点Ｂ（０,ｂ）关于直线ｘ＝ｋ（ｋ≠０）的对称点Ｂ′（２ｋ,ｂ）不在椭圆Ｃ图１上,故直线ｘ＝ｋ（ｋ≠０）不是椭圆Ｃ的对称轴．设Ｆ１,Ｆ２是椭圆Ｃ的两个焦点,椭圆Ｃ的长轴Ａ１Ａ２关于直线ｌ：ｙ＝ｋｘ＋ｎ（ｋ,ｎ至少有一个不等于零）的…     

Bonnesen等周不等式的一个初等证明

本文给出Bonnesen等周不等式的一个初等证明,它不涉及积分几何理论,浅显易懂.     

数学定理的机械化证明

1946年电子计算机诞生。4年后的1950年波兰数学家塔斯基(Tarslci,1901-1983)证明：一切初等几何和初等代数范围的命题,都可以用机械化方法判断其真伪,使人们大吃一惊。     

费尔马小定理的一个初等证明

利用多元多项式定理,给出费尔马小定理的一种完全初等的证明.     

微分中值定理证明小议

<正> 拉格朗日中值定理和柯西中值定理是通过构造辅助函数并利用罗尔定理证明的.初学对此感到陌生,难以接受.一般是从几何直观入手引入辅助函数,但初学者还认为思路不自然. 这篇小议对构造辅助函数给出另外的两条思路,而且不是从几何直观,纯粹从定理的结论入手,进行逆推,以求使读者感到构造辅助函数是水到渠成,不勉强.但愿此文能对大家有所启发,初步掌握构造性证明的方法.