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.     

质点法在SGARP中的新实现

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

Symmetry via spherical reflection

In 1955 Alexandrov [2, 7, p. 147] introduced the method of planar reflection as a procedure for proving symmetry of closed surfaces of constant mean curvature. In subsequent years, a number of refinements were given, and the method was applied successfully to other problems in differential geometry and partial differential equations, cf. [10, 5, 12, 9, 3, 12]. In the present paper, we introduce a new procedure for obtaining symmetry which may be considered an extension of the planar reflection method to reflection about spheres. In the interest of clearly delineating the new features of the method, in this initial presentation we give a new proof of the original Alexandrov theorem: A closed embedded surface of constant mean curvature in Euclidean space is a round sphere. Our proof of this result is not simpler than that of Alexandrov; it is, however, different in some crucial respects. Our justification for introducing the new procedure lies in its applicability to configurations that are not accessible to planar reflection arguments. In particular, we use the new method in [8] to prove the non-existence in certain cases of embedded liquid bridges joining two planes that meet to form a wedge domain, a result whose interest derives in turn largely from the fact that under the same (physical) boundary conditions embedded bridges do exist and can be stable when the planes are parallel. The method of spherical reflection as presented below relies on a new maximum principle related to surface geometry, which we believe to have independent interest. Further, the method utilizes a peculiar characterization of spherical surfaces by aggregate symmetry, which should also have interest for other problems arising in the global differential geometry of surfaces.     

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

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

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…     

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

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

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.     

几何定理机器证明三十年

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

Metric Uniformization and Spectral Bounds for Graphs

We present a method for proving upper bounds on the eigenvalues of the graph Laplacian. A main step involves choosing an appropriate “Riemannian” metric to uniformize the geometry of the graph. In many interesting cases, the existence of such a metric is shown by examining the combinatorics of special types of flows. This involves proving new inequalities on the crossing number of graphs.     

Géométrie de la chaînette ou hypergéométrie

Summary Differential calculus is proving inefficient to solve problems of mechanics dealing with ropes, unless one satisfies oneself with rough approximations.Ordinary or Euclidean geometry is also proving useless: The author shows that in order to solve such problems as described before, one has to use a special branch of geometry. Distances are no longer measured along rigid straight rules, but along the catenary curves in question.The fundamental characteristics of this hypergeometry, with some of their more striking results, are described in the following study.     

基于初等几何方法的π数值计算的探索实验

探讨了基于初等几何方法的圆周率π的数值计算的探索数学实验教学.展现了整个实验的实验设计,数据分析,发现、估计及验证规律的全过程.     

A locking-free approximation of curved rods by straight beam elements

Summary. We consider an elastic model for a curved rod with arbitrary three-dimensional geometry, incorporating shear and membrane as well as bending and torsion effects. We define an approximation procedure based on a discretization by linear Timoshenko beam elements. Introducing an equivalent mixed problem, we establish optimal error estimates independent of the thickness, thereby proving that shear and membrane locking is avoided. The approximation scheme is tested on specific examples and the numerical results confirm the estimates obtained by theory. Received May 31, 1995 / Revised version received February 26, 1996     

局部对称共形平坦黎曼流形中的紧致子流形

本文研究局部对称共形平坦黎曼流形中具有平行平均曲率向量的紧致子流形的性质，通过一个代数不等式的证明，改进了已有的结果．     

High school students’ perceptions of geometrical proofs proving and refuting geometrical claims of the ‘for every … ’ and ‘there exists’ type

Proving and refuting mathematical claims constitute a significant element in the development of deductive thinking. These issues are mainly studied during geometry lessons and very little (if at all) in lessons of other mathematical disciplines. This study deals with high school students’ perceptions of proofs in the geometry. The study explores whether students know when to use a deductive proof and when an example is sufficient for proving or refuting geometrical claims. The findings indicate that in cases of simple claims, the students corroborate them by using a deductive proof. However, when the claim is more complex, the students tend to present both a proof and an example. Moreover, they are unsure whether using an example can constitute a method for proving a mathematical claim, believing that in mathematics everything must be proven. They believe that examples are used merely for illustration purposes rather than as a means of convincing. The research conclusions support the need for deepening and developing the students’ distinction between cases where examples are insufficient and cases where an example is sufficient for proving a claim.     

Die Innenwelt des Beweisens im Mathematikunterricht

This empirical study reports on proving processes in everyday classroom practices in French and German geometry teaching. Classroom observations and comparative analyses presented in the study focus on units in which the Pythagorean Theorem was taught. The theoretical framework is based on epistemological and didactical research that asserts that justification and development of knowledge cannot be separated from each other within proving, nor can they be separated from their context of origination. This suggests a dialectic understanding of proofs which is in fact the theoretical basis of this study. From this perspective the empirical study first addresses the mathematical contexts of the proving processes in the units observed and then analyses argumentations within these processes.     

基于二元语义的高原地区航材配送中心选址决策研究

针对高原地区航材配送中心选址决策特点,构建了航材配送中心选址指标体系,提出了基于二元语义的群决策选址方法,给出了基于二元语义群决策的航材配送中心选址步骤.通过实例得出了备选点的综合评价值,证明了该方法的有效性.     

基于二元语义的高原地区航材配送中心选址决策研究

针对高原地区航材配送中心选址决策特点,构建了航材配送中心选址指标体系,提出了基于二元语义的群决策选址方法,给出了基于二元语义群决策的航材配送中心选址步骤.通过实例得出了备选点的综合评价值,证明了方法的有效性.     

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.     

Periodic Homogenization of Parabolic Nonstandard Monotone Operators

We study the periodic homogenization for a family of parabolic problems with nonstandard monotone operators leading to Orlicz spaces. After proving the existence theorem based on the classical Galerkin procedure combined with the Stone-Weierstrass theorem, the fundamental in this topic is the determination of the global homogenized problem via the two-scale convergence method adapted to this type of spaces.     

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)