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

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

例证法与代数簇的包含关系

1986年,洪加威教授发展吴文俊机器证明理论,提出了一类平面几何定理的例证法,这一方法依赖于 Ritt-吴整序原理和吴文俊教授关于升组不可约分解的构造性理论.我们发现例证法适用于证明所有等式型几何定理,即吴几何中的定理.本文应用吴和洪的方法叙述等式型几何定理的例证法,并考虑代数簇的包含关系.目前的讨论仅停留在理论上,这种方法能否用来证明非平凡的几何定理还有待于进一步研究和尝试.     

多项式复根的分离方法——Wu-Ritt 原理的一个应用

计算机的出现,为数学研究提供了强有力的手段,并激起了机械化与构造化的新浪潮.60年代后期开始,计算机代数异军突起,受到人们广泛关注.其中,吴文俊教授1978年在研究几何定理机器证明的过程中,提出了 Wu-Ritt 整序原理,并以此成功的解决了相当一大类几何定理的机器证明.不仅如此,随后的进一步研究工作表明,Wu-Ritt 原     

关于多项式的因子分解的机械方法的注记

在Van der Waerden [1]的§37中有一个定理说:如果域△上的单变量的多项式能在有限步内分解,则多变量的多项式亦可。由于这一定理对几何证明的机械化方法颇为重要,吴文俊在总结他自己所开创的几何定理机器证明的重要著作[2]的4.2中以如下形式重新叙述并证明了上述的定理: 设A是一个有么元素的整环,且已知有一机械方法可在有限步内将A中任意一数唯一分解成不可约因子(确定至A中可逆因子),则有一机械方法可在有限步内将A[x_1,     

推出“规则化商除法”

中国科学院院士吴文俊先生指出:“数学问题的机械化,就要求在运算或证明过程中,每前进一步之后,都有一个确定的,必须选择的下一步,这样沿着一条有规律的、刻板的道路,一直达到结论。”“我国古代数学的精髓是一种机械化的思想和机械化的方法,正好符合现时代的要求和状况。因此,我觉得对中国古代数学要特别加以重视。”     

抓住向量的核心知识，灵活解决问题

向量是近代数学中重要和基本的数学概念之一,它可以沟通代数、几何与三角函数,也是考查学生思维能力很好的载体,因此向量是高考的重点内容之一．向量的核心内容可以概括成“两个定理、三种形式、四类运算”．两个定理是指共线向量性质定理和平面向量基本定理;三种形式为几何形式（作图）、代数形式、坐标形式;     

推出“规则化商除法”

中国科学院院士吴文俊先生指出：“数学问题的机械化，就要求在运算或证明过程中，每前进一步之后，都有一个确定的，必须选择的下一步，这样沿着一条有规律的、刻板的道路，一直达到结论．”“我国古代数学的精髓是一种机械化的思想和机械化的方法，正好符合现时代的要求和状况．因此，我觉得对中国古代数学要特别加以重视。”     

n维双曲空间和n维球面空间中的正弦定理及应用(英文)

本文研究了n维双曲空间和n维球面空间中单形的正弦定理和相关几何不等式.应用距离几何的理论和方法,给出了n维双曲空间和n维球面空间中一种新形式的正弦定理,利用建立的正弦定理获得了Hadamard型和Veljan-Korchmaros型不等式.另外,建立了涉及两个n维双曲单形和n维球面单形的"度量加"的一些几何不等式.     

解三角形常用方法举例

<正>初中几何中三角形的计算基本都会涉及到勾股定理和锐角三角函数.勾股定理只能解决三角形边的问题,但要涉及到边角运算就须运用锐角三角函数,但锐角三角函数由于其公式的灵活多变同学们都不易掌握.下面就解三角形中常用的一些方法进行简单的讲解.一、用定义充分利用锐角三角函数的定义及边角关系解答.     

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

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

A new theorem discovered by computer prover

Concerning Pappus lines and Leisenring lines there is a set of interesting theorems given in [1]. In this paper, we show that these theorems can be easily proved by our computer prover which is implemented on the basis of Wu's method for mechanical theorem proving in geometries. Using this prover we discovered, furthermore, a new theorem: The six intersection points of every Pappus line and its corresponding Leisenring line are collinear.     

几何定理机器证明三十年

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

Channels with arbitrarily varying channel probability functions in the presence of noiseless feedback

In this article we study a channel with arbitrarily varying channel probability functions in the presence of a noiseless feedback channel (a.v.ch.f.). We determine its capacity by proving a coding theorem and its strong converse. Our proof of the coding theorem is constructive; we give explicitly a coding scheme which performs at any rate below the capacity with an arbitrarily small decoding error probability. The proof makes use of a new method ([1]) to prove the coding theorem for discrete memoryless channels with noiseless feedback (d.m.c.f.). It was emphasized in [1] that the method is not based on random coding or maximal coding ideas, and it is this fact that makes it particularly suited for proving coding theorems for certain systems of channels with noiseless feedback.As a consequence of our results we obtain a formula for the zero-error capacity of a d.m.c.f., which was conjectured by Shannon ([8], p. 19).     

质点法在SGARP中的新实现

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

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.     

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

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

Two Hardy-Bennett-Type Theorems

The factorization of inequalities is a new and very effective method proving the best possible version of classical and recent inequalities. Presently we shall slightly improve two factorization theorems proved by us, and simultaneously verify the theorem of [2] in its original form. This revised version was published online in June 2006 with corrections to the Cover Date.     

Quantifier elimination for the theory of algebraically closed valued fields with analytic structure

The theory of algebraically closed non‐Archimedean valued fields is proved to eliminate quantifiers in an analytic language similar to the one used by Cluckers, Lipshitz, and Robinson. The proof makes use of a uniform parameterized normalization theorem which is also proved in this paper. This theorem also has other consequences in the geometry of definable sets. The method of proving quantifier elimination in this paper for an analytic language does not require the algebraic quantifier elimination theorem of Weispfenning, unlike the customary method of proof used in similar earlier analytic quantifier elimination theorems. (© 2007 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

A new proof of the stable manifold theorem for hyperbolic fixed points on surfaces

We introduce a new technique for proving the classical stable manifold theorem for hyperbolic fixed points. This method is much more geometrical than the standard approaches which rely on abstract fixed point theorems. It is based on the convergence of a canonical sequence of “finite time local stable manifolds” which are related to the dynamics of a finite number of iterations.     

A generalized Kantorovich theorem for nonlinear equations based on function splitting

The Kantorovich theorem is a fundamental tool in nonlinear analysis for proving the existence and uniqueness of solutions of nonlinear equations arising in various fields. In the present paper we formulate and prove a generalized Kantorovich theorem that contains as special cases the Kantorovich theorem and a weak Kantorovich theorem recently proved by Uko and Argyros. An illustrative example is given to show that the new theorem is applicable in some situations in which the other two theorems are not applicable.