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.     

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.     

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

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

Conjugate connections and Radon's theorem in affine differential geometry

For a given nondegenerate hypersurfaceM ⁿ in affine space ? ⁿ⁺¹ there exist an affine connection ?, called the induced connection, and a nondegenerate metrich, called the affine metric, which are uniquely determined. The cubic formC=?h is totally symmetric and satisfies the so-called apolarity condition relative toh. A natural question is, conversely, given an affine connection ? and a nondegenerate metrich on a differentiable manifoldM ⁿ such that ?h is totally symmetric and satisfies the apolarity condition relative toh, canM ⁿ be locally immersed in ? ⁿ⁺¹ in such a way that (?,h) is realized as the induced structure? In 1918J. Radon gave a necessary and sufficient condition (somewhat complicated) for the problem in the casen=2. The purpose of the present paper is to give a necessary and sufficient condition for the problem in casesn=2 andn≥3 in terms of the curvature tensorR of the connection ?. We also provide another formulation valid for all dimensionsn: A necessary and sufficient condition for the realizability of (?,h) is that the conjugate connection of ? relative toh is projectively flat.     

编序式问卷调查的模糊偏序排序法

讨论了现有的编序式问卷调查排序方法的不足之处;提出了基于模糊偏序关系的编序式问卷调查的排序方法,给出了模糊偏序排序法的数学模型,论证了用模糊偏序关系对编序式问卷调查进行排序是一种较好的方法;并用实例分析了模糊偏序排序法应用于编序式问卷调查的具体操作步骤.     

一个组面试问题的最佳顺序安排

采用边界阶段方法讨论最优组面试问题的最佳划分选择策略,在允许调整面试顺序的情况下,得到最优组面试问题中如何重新安排面试顺序能够以最大概率录用到最优应聘者的排序策略.     

关于矩阵的Sharp序、*序和减序

给出短阵sharp序的一个新的刻画，由此得到(半)正定短阵sharp序与其平方矩阵sharp序之间的关系．我们还讨论正规矩阵的*序与减序之间的关系，推广了关于Hermmite矩阵的相应结果．     

Induction and Skolemization in saturation theorem proving

We consider a typical integration of induction in saturation-based theorem provers and investigate the effects of Skolem symbols occurring in the induction formulas. In a practically relevant setting we establish a Skolem-free characterization of refutation in saturation-based proof systems with induction. Finally, we use this characterization to obtain unprovability results for a concrete saturation-based induction prover.     

A symbolic finite-state approach for automated proving of theorems in combinatorial game theory

We develop a finite-state automata approach, implemented in a Maple package Toads and Frogs available from our websites, for conjecturing, and then rigorously proving, values for large families of positions in Richard Guy's combinatorial game ‘Toads and Frogs’. In particular, we prove a conjecture of Jeff Erickson.     

NBU(2)性的偏序刻画

为刻画同一寿命分布类中两个不同分布的NBU(2)性的强弱,本文定义了一个新的偏序,即NBU(2)序,并证明NBU(2)序具有反身性,反对称性和传递性.另外,该偏序与超可加序、NBUE序,增凹序的关系也作了探讨.基于被比较分布是指数的情况,还建立了判定NBU(2)序的一个充要条件.     

On free abelian categories for theorem proving

We give a computational approach to theorem proving in homological algebra. This approach is based on computations in the free abelian category of an additive category A. We show that the free abelian category is amenable to explicit computations whenever we can decide homotopy equations in A. As some consequences of our investigations, we recover Dowker's explicit formula for the connecting homomorphism ? in the snake lemma, we find a universal sense in which ? is unique, and we give a refined version of the 5-lemma.     

Ordering trees by their spectral radii

Let T be a tree with n vertices and let A（T） be the adjacency matrix of T. Spectral radius of T is the largest eigenvalue of A（T）. Wu et al. [Wu, B.F., Yuan, X.Y, and Xiao, E.L. On the spectral radii of trees, Journal of East China Normal University （Natural Science）, 3：22-28 （2004）] determined the first seven trees of order n with the smallest spectral radius. In this paper, we extend this ordering by determining the trees with the eighth to the tenth smallest spectral radius among all trees with n vertices.     

列序压缩算子的不动点和Hammerstein型积分方程

给出了Banach空间列序压缩算子定义,讨论了此类算子不动点存在性问题和其在非线性H amm erste in型积分方程中的应用.     

A view of automated proof checking and proving

Different techniques of automated formal reasoning are described and their performance and requirements on the human user are evaluated. The main trade-off is between autonomy and flexibility in conducting proofs. Examples of the use of techniques and existing systems are given, but not attempt of an exhaustive overview is made. The goal is to provide the reader with an idea of what to look for when selecting an approach for his/her application.     

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.     

Equality in Distribution in a Convex Ordering Family

Let F and G be the respective distributions of nonnegative random variables X and Y satisfying the convex ordering. We investigate the class of functions h for which the equality E[h(X)] = E[h(Y)] guarantees F = G. It leads to extensions of some existing results and at the same time offers a somewhat simpler proof.     

四元数矩阵的极分解及其GL偏序

本文给出了四元数矩阵的唯一极分解定理和两个四元数矩阵可同时极分解的两种刻画；进而引进了四元数矩阵的GL偏序的概念，它是重要的Lǒwner偏序的一般化，并得到这个新偏序的6种刻画．     

关于排序不等式的一个简单证明

利用Abel变换,给出排序不等式的证明,并对等号成立问题作了进一步的讨论.