几何定理机器证明三十年

由于传统的兴趣和多种原因,几何定理的机器证明在自动推理的研究中占有重要的地位.自吴法发表至今30年,几何定理机器证明的研究和实践有了很大的进展.对无序几何命题而言,代数方法、数值方法均能有效地判定其真假,面积法(消点法)、搜索法更能生成其可读的证明.几何不等式机器证明的研究,由于多项式完全判别系统的建立,也有了突破.研究领域已由机器证明扩展为包括几何作图在内的一般几何问题的机器求解,并有了实际的应用.     

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

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

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

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

几何定理机器证明的WE完全方法

在几何定理机器证明的各种方法中，吴氏方法获得了显著的成功．如预先把有关代数簇分解为不可约簇，则吴氏方法可成为完全方法．本文在吴法的基础上，以辗转伪除法为辅助工具，发展出一种不必预先分解代数簇的完全方法，并给出一些手算实例．     

几何定理机器证明的结式矩阵法

本文提出了一种不必预先分解升列为不可约于列而克服所谓“可约性困难”的方法．由于使用了吴除法及子结式计算，我们也称这种方法为ＷＲ分解算法．     

初等几何定理机器证明——吴方法简介

吴文俊院士获得2000年国家科学技术最高奖,这对我们数学工作者是极大的鼓舞,他的主要成就包括代数拓扑,应用数学,数学史,几何定理的机器证明等．这里,我们介绍后者．     

初等几何定理机器证明中的可约性问题

在几何定理的机器证明中,遇到可约的情形就会出现重大困难。本文依据代数几何中代数簇相对可约与绝对可约的概念,引进直线与园的定向座标,以避免或至少减轻可约性的困难。作为应用实例,我们对割线定理、Feuerbah 定理以及 Thebault-Taglor-Chou 定理进行了分析,并对最后一个定理给出了比已知要简单得多的机器证明。     

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

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

基于指标形式张量的微分几何定理机器证明

提出了一个基于指标形式张量的微分几何定理的机器证明算法.该算法将微分几何定理转化成带指标的张量多项式的计算问题,然后通过利用重写规则,挖掘等价条件和分次选取条件等方法大大减少了这个多项式系统的方程个数.再利用这个多项式系统本身和关于哑元的方程三角化这个多项式系统,将所得到的首项代入结论, 从而得到了该定理的机器证明.该算法不仅能够证明基于指标形式张量的微分几何定理,也可以用于张量方程的求解.     

一类初等微分几何定理机器证明的算法与实现

空间曲面上的曲线论是初等微分几何的重要部分．作者提出了一种以外微分运算和向量计算为主要工具,可以进行有关曲面上曲线局部性质的定理机器证明的算法．该算法结合了曲面上的活动标架,曲面上曲线的测地标架和曲线自身的Frenet标架,在Maple 9下得到实现．对20个例子进行的测试表明,由该算法生成的自动证明简短可读．     

几何定理机器证明的方法--吴方法思想的形成

计算机在自己发展的早期就与数学结下了不解之缘 .众所周知 ,数值计算无论是在数学发展之初 ,还是现在 ,甚至在未来的数学发展中都将占据着至关重要的地位 .因此 ,在解决越来越复杂的数值计算过程中 ,世界各民族都创造了各式各样的计算工具 :屈指计算 →卵石计算 (结绳计算、刻痕计算 ) →算筹 →算盘→计算尺 →…… ,而计算机成了数值计算工具中的佼佼者 ,从手摇 (机械 )计算机 →电动 (机械 )计算机 →直到现在发展的高速电子计算机 (电脑 ) .计算机作为数值计算工具的发明要归功于 1 5世纪法国著名的数学家、物理学家和思想家帕斯卡 (B…     

基于多项式组主项解耦消元法的几何定理机器证明

基于多项式组主项解耦消元法 ,将几何定理的假设条件 (多项式组 PS)化为主项只含主变元的三角型多项式组 DTS,可得到定理命题成立的不含变元的非退化条件 ,即充分必要或更接近充分必要的非退化条件 .由于多项式主系数不含变元 ,已不存在 DTS多项式之间的约化问题 ,故方法有普遍意义 .文中例为西姆松定理的机器证明 .     

仿射括号代数理论与算法及其在几何定理机器证明中的应用

主要讨论仿射括号代数的理论与算法及其在定理机器证明中的应用。文中首次提出了边界扩张算法等几个有效的仿射括号代数算法, 同时分析了边界算子的性质, 为系统实现奠定了基础. 文中也提及了单括号因子整除判定、单项式因子整除判定、仿射几何的构造和对应表示表示等工作. 在符号计算软件 Maple 10中, 应用上述理论与算法实现了仿射几何的定理机器 证明, 并用大约100多个例子进行了测试, 之后将结果进行了比较.     

一个几何定理的面积证明

<正>~~     

Clifford链定理简单的几何证明

1引言文[1]介绍了一个美丽的定理,即Clifford链定理.两条直线交于一点,称此点为两线的2级Clifford点(简称2级点);三条直线确定的3个2级点共圆,称之为这3条直线的3级Clifford圆(简称3级圆);在这平凡事实的基础上,意外地有著名的:     

几个初等几何定理的证明

近閱讀叶菲莫夫著高等几何学,發觉其中有几个定理,可作更直接的証明,茲介紹如下(本文所指頁数系俄文原著第三版).     

Mazur定理的一个推广及其几何证明

建立了代数内点的若干性质；给出了Mazur定理的一个推广及其几何证明；证明了此推广的Mazur定理与基本分离定理等价；还得到一个严格分离定理．     

初等几何定理证明的Clifford代数方法

本文结合是吴方法及平面几何的Ｃｌｉｆｆｏｒｄ代数表示，提出了几何定理机器证明的一种完备的方法，用这种方法证明定理时，三角化的过程及证明的过程通常较以前的方法更简短而且它们是可以几何解释的。     

能用例证法来证明几何定理吗?

本文提出了证明平面几何定理的例证法。根据这一方法,想判定一个几何命题是否为真,只需近似地验证一个数值曲特例就行了。这个特例仅依赖于该几何命题在某种规范形式下表述的长度l以及命题中自由变量的个数s,可以非常简单地表示出来,与几何命题的内容无关。同时还证明了该类平面几何判定问题所需的并行时间是l_s的一个多项式。     

一对几何定理的证明与一类趣题

<正>本文拟证明一对几何定理,并运用其证明一类有趣的几何问题.1.定理及证明定理1如图1,⊙O1与⊙O2内切于点P,过⊙O1上的点A作⊙O2的切点AB,切线为B,设⊙O1与⊙O2的半径分别为R与r,则有AP=