质点法在SGARP中的新实现

可持续发展的几何自动推理平台(SGARP)支持用户发展多种多样基于规则的机器自动推理或人机交互推理方法,但缺乏处理符号计算的模块,其解题能力仍有待加强.质点法是最近发展的继面积法之后又一个能对可构造型几何命题生成可读机器证明的具有完全性的算法.基于一种在SGARP中快捷实现符号计算功能的方法,对质点法机器证明算法进行了新的实现.新添加的质点法模块使得用户能更便捷地验证更多的几何定理,从而使SGARP能更好地满足用户学习与发展几何机器推理的需求.     

基于吴方法的几何定理证明的恒等式方法

多年来通常认为以吴方法为代表的几何定理机器证明的坐标法给出的证明不可读,或不是图灵意义下的类人解答.其实,只要对吴氏的算法做不多的改进,即将命题的结论多项式表示为其条件多项式的线性组合,就能获得不依赖于理论、算法和大量计算过程的恒等式明证.这样的恒等式可以转化为其他更简明且更有直观几何意义的点几何形式或向量及其他形式,从而获得多种证明方法.这也证明了点几何恒等式明证方法对等式型几何命题的普遍有效性.     

基于特征列方法和Wronskian行列式的曲面定理机器证明

将Chou与Gao的关于微分几何中曲线定理机器证明的方法推广到微分几何曲面定理中. 改进了经典的Wronskian行列式, 它可以用于判断微分域中的有限个元素是否在其常数域上线性相关. 基于Wronskian行列式, 可以用代数语言来描述微分几何曲面理论中的几何表述, 进而用特征列方法来证明这些定理.     

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

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

Proving Theorems in Elementary Geometry with Clifford Algebraic Method

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

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

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

消点法解题数例分析

中国科学院院士张景中教授在攻克计算机的可读性证明时创立了平面几何命题论证的“消点法” .众所周知 ,机器证明是现代数学 (计算机 )对科学的重大贡献 ,自吴文俊教授创立了吴方法之后 ,这项研究取得了突破性的进展 ,但其证明方式仍是“纯机器”的———采用的是非常规的语言 ,不能被一般的人“读”懂 .中国科学院院士张景中教授首创机器的可读性证明 ,使我国在机器证明这一尖端领域的研究水平无可置疑地处于世界领先地位 .这是继“吴方法”之后更辉煌的成就 .有趣的是 ,机器证明中使用的“消点法”不仅适用于机器推理 ,而且还可“手工”操…     

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

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

图表追踪的一种机器实现方法

交换图表追踪法是同调代数中一种重要的证明方法.本文提出了一种基于前推的交换图表追踪的机器实现方法,它可以证明同调代数中一系列基于交换图的定理.该方法从定理的结论出发,通过构造辅助元素以及对辅助元素进行推导,能在有限步内给出定理的证明.本文提出的前推方法已经在Java开发平台上实现,同调代数中的五引理、九引理、蛇引理等的证明都可以由我们的程序自动产生.     

基于Coq的第三代微积分机器证明系统

本文基于证明辅助工具Coq,完整实现林群院士和张景中院士等倡导的第三代微积分|没有极限的微积分|理论构架的形式化验证,包括对张景中等发表的题为\微积分基础的新视角"论文中全部定义和定理的Coq描述.进而,对定理无例外地给出Coq的机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可靠.本文是实践研究人员利用计算机学习、理解、构建乃至教育现代数学理论的一个尝试.     

Clifford 代数,几何计算和几何推理

Clifford代数是一种深深根植于几何学之中的代数系统,被它的创始人称为几何代数．历史上,E．Cartan,R．Brauer,H．Weyl,C．Chevalley等数学大师都曾研究和应用过Clifford代数,对它的发展起了重要作用．近年来,Clifford代数在微分几何、理论物理、经典分析等方面取得了辉煌的成就,是现代理论数学和物理的一个核心工具,并在现代科技的各个领域,如机器人学、信号处理、计算机视觉、计算生物学、量子计算等方面有广泛的应用．本文主要介绍Clifford代数在几何计算和几何推理中的应用．作为一种优秀的描述和计算几何问题的代数语言,Clifford代数对于几何体,几何关系和几何变换有不依赖于坐标的、易于计算的多种表示,因而应用它进行几何自动推理,不仅使困难定理的证明往往变得极为简单,而且能够解决一些著名的公开问题,目前在国际上,几何自动推理已经成为Clifford代数的一个重要应用领域。     

Mechanical theorem proving in differential geometry

An automated reasoning method, based on Wu’s method and calculus of differential forms, is proposed for mechanical theorem proving in local theory of space surfaces in differential geometry. The method has been used to simplify one of Chem’s theorems: “The non-trivial families of isometric surfaces having the same principal curvatures are W-surfaces.” Some other theorems are also tested by this method. The proofs are generally simpler than those in differential geometry textbooks. Project supported partially by the National Natural Science Foundation of China.     

On the Unavoidable Uncertainty of Truth in Dynamic Geometry Proving

The aim of this note is to discuss some issues posed by the emergency of universal interfaces able to decide on the truth of geometric statements. More specifically, we consider a recent GeoGebra module allowing general users to verify standard geometric theorems. Working with this module in the context of Varignon’s theorem, we were driven—by the characteristics of the GeoGebra interface—to perform a quite detailed study of the very diverse fate of attempting to automatically prove this statement, when using two different construction procedures. We highlight the relevance—for the theorem proving output—of expression power of the dynamic geometry interface, and we show that the algorithm deciding about the truth of some—even quite simple—statements can fall into a not true and not false situation, providing a source of confusion for a standard user and an interesting benchmark for geometers interested in discovering new geometric facts.     

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

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

ORDERING IN AUTOMATED THEOREMPROVING OF DIFFERENTIAL GEOMETRY

1.BackgroundMom1979,WuWentsunbeganthestudyofautomatedtheoremprovingindifferentialgeometry[1].Inhismethod,thehypotheses,representedbydifferentialpolynomials,aretriangulatedaccordingtoanorderofthevariablesinthepolynomials;theconclusionisprovedbythetriangulatedresultcalledcharacteristicset.Wuusedelement-basedorderingmethodwhichcanbeillustratedbythisexample'LettingxKybetwosmoothfunctionsofthesamevariable,thenxKX'KX"K'Ky'y,Ky"'.ThisorderisthefoundationofWu'seliminationprinciple.However,a…     

Napoleon’s quasigroups

Napoleon’s quasigroups are idempotent medial quasigroups satisfying the identity (ab·b)(b·ba) = b. In works by V. Volenec geometric terminology has been introduced in medial quasigroups, enabling proofs of many theorems of plane geometry to be carried out by formal calculations in a quasigroup. This class of quasigroups is particularly suited for proving Napoleon’s theorem and other similar theorems about equilateral triangles and centroids.     

Mechanical theorem proving in the surfaces using the characteristic set method and Wronskian determinant

In this paper, we generalize the method of mechanical theorem proving in curves to prove theorems about surfaces in differential geometry with a mechanical procedure. We improve the classical result on Wronskian determinant, which can be used to decide whether the elements in a partial differential field are linearly dependent over its constant field. Based on Wronskian determinant, we can describe the geometry statements in the surfaces by an algebraic language and then prove them by the characteristic set method.     

Ordering in mechanical geometry theorem proving

Ordering in mechanical geometry theorem proving is studied from geometric viewpoint and some new ideas are proposed. For Thebault’s theorem which is the most difficult theorem that has ever been proved by Wu’s method, a very simple proof using Wu’s method under a linear order is discovered. Project supported by the National Natural Science Foundation of China.