消点法解题数例分析

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

天堑变通途——《初等几何研究(第2版)》代序

由我国著名数学家吴文俊、张景中两位院士分别创建的两种几何定理机器证明,使我国在这一领域处于世界领先地位,正如王梓坤院士讲的,"我们可以自豪地说,几何定理机器证明研究的重大成果都是由我国数学家所取得的",可是,长期以来都以为行之有效的机器证明深奥难懂,因而影响了它的普及,现在本书深入浅出的讲解,已得到两位院士的肯定,张景中给作者的回信称"阐述非常到位,不仅详略得当而且有独到的评述",这里转载陆汝钤院士为本书写的序,帮助我们了解一下机器证明的发展和现状.     

微分积分定义的几种新途径对比分析

微分与积分的常规定义具有复杂性且两者之间缺乏直观的联系.对于项武义教授、张景中院士与林群院士所给出的新定义进行一一阐述,然后从概念引入、微分与积分之间的联系、定义的应用效果以及微积分基本定理的所指这四个方面进行比较分析.对微积分阐释途径的多元化研究,有助于教改的推进与完善.     

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

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

机器证明的回顾与展望

机器证明的回顾与展望张景中（中国科学院成都计算机应用研究所）机器证明及其应用，是我国攀登计划项目之一．项目核心内容主要是几何定理机器证明和非线性代数方程组理论、算法和应用．实际上，机器证明研究领域的范围要广泛得多．在国外更一般地叫做自动推理．我们把几...     

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

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

关于数学证明方法与算法实现关系的一些探讨

从数学证明和程序设计的角度,分析比较了数学命题定理证明中常用的数学归纳法、递推算法、递归算法、反证法等数学方法.讨论了它们在理论证明、算法实现方面的联系和优缺点,提出教学中的一些建议.     

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

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

学习“微积分之前可以做些什么”一文后的若干思考

<正>最近学习了林群、张景中院士的"微积分之前可以做些什么"一文,这是一篇阐述如何将微积分改造成比较容易理解的第三代微积分的文章,是一篇教育数学的有价值的代表作.读此文后,我思考的问题是能否把这些内容真正落实到中学的教学中,现谈一些粗浅的体会,向两位院士请教.1 微积分进入中学教学的争论微积分进入我国中学数学教材是2004年以后的事,解放后的中学数学一直没有这个内容.对于微积分进入中学,在当初讨论高中数学课程标准时,曾经有过两种不     

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

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

Formal specification and proofs for the topology and classification of combinatorial surfaces

We describe one of the first attempts at using modern specification techniques in the field of geometric modeling and computational geometry. Using the Coq system, we developed a formal multi-level specification of combinatorial maps, used to represent subdivisions of geometric manifolds, and then exploited it to formally prove fundamental theorems. In particular, we outline here an original and constructive proof of a combinatorial part of the famous Surface Classification Theorem, based on a set of so-called “conservative” elementary operations on subdivisions.     

Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs

Numerical programs may require a high level of guarantee. This can be achieved by applying formal methods, such as machine-checked proofs. But these tools handle mathematical theorems while we are interested in C code, in which numerical computations are performed using floating-point arithmetic, whereas proof tools typically handle exact real arithmetic. To achieve this high level of confidence on C programs, we use a chain of tools: Frama-C, its Jessie plugin, Why and provers among Coq, Gappa, Alt-Ergo, CVC3 and Z3. This approach requires the C program to be annotated: each function must be precisely specified, and we prove the correctness of the program by proving both that it meets its specifications and that no runtime error may occur. The purpose of this paper is to illustrate, on various examples, the features of this approach.     

A case study in formalizing projective geometry in Coq: Desargues theorem

Formalizing geometry theorems in a proof assistant like Coq is challenging. As emphasized in the literature, the non-degeneracy conditions lead to long technical proofs. In addition, when considering higher-dimensions, the amount of incidence relations (e.g. point–line, point–plane, line–plane) induce numerous technical lemmas. In this article, we investigate formalizing projective plane geometry as well as projective space geometry. We mainly focus on one of the fundamental properties of the projective space, namely Desargues property. We formally prove that it is independent of projective plane geometry axioms but can be derived from Pappus property in a two-dimensional setting. Regarding at least three-dimensional projective geometry, we present an original approach based on the notion of rank which allows to describe incidence and non-incidence relations such as equality, collinearity and coplanarity homogeneously. This approach allows to carry out proofs in a more systematic way and was successfully used to fairly easily formalize Desargues theorem in Coq. This illustrates the power and efficiency of our approach (using only ranks) to prove properties of the projective space.     

Designing and proving correct a convex hull algorithm with hypermaps in Coq

This article presents the formal design of a functional algorithm which computes the convex hull of a finite set of points incrementally. This algorithm, specified in Coq, is then automatically extracted into an OCaml program which can be plugged into an interface for data input (point selection) and graphical visualization of the output. A formal proof of total correctness, relying on structural induction, is also carried out. This requires to study many topologic and geometric properties. We use a combinatorial structure, namely hypermaps, to model planar subdivisions of the plane. Formal specifications and proofs are carried out in the Calculus of Inductive Constructions and its implementation: the Coq system.     

关于离散Karamata不等式及其应用

本文获得了著名Karamata不等式的离散形式，利用这个结果推广了Newton不等式，应用推广的Newton不等式将张景中和杨路在[1]所得的几何不等式加以推广。     

Probabilistic verification of proofs in calculuses

We define a special kind of a probabilistically checkable proof system, namely, probabilistically checkable proof calculuses (PCP calculuses). A proof in such a calculus can be verified with sufficient confidence by examining only one random path in the proof tree, without reading the whole proof. The verification procedure just checks all applications of inference rules along the path; its running time is assumed to be polynomial in the theorem length. It is shown that the deductive power of PCP calculuses is characterized as follows: (i) the decision problem for theorems is in PSPACE for all PCP calculuses; and (ii) the mentioned problem is PSPACE-hard for some of the calculuses. Bibliography: 14 titles. Translated fromZapiski Nauchnykh Seminarov POMI, Vol. 241, 1997, pp. 97–116 This research was supported in part by the Russian Foundation for Basic Research. Translated by E. Ya. Dintsin.     

On the different ways that mathematicians use diagrams in proof construction

The processes by which individuals can construct proofs based on visual arguments are poorly understood. We investigated this issue by presenting eight mathematicians with a task that invited the construction of a diagram, and examined how they used this diagram to produce a formal proof. The main findings were that participants varied in the extent of their diagram usage, it was not trivial for participants to translate an intuitive argument into a formal proof, and participants’ reasons for using diagrams included noticing mathematical properties, verifying logical deductions, representing ideas or assertions, and suggesting proof approaches.     

The polynomial bounds of proof complexity in Frege systems

The concept of a determinative set of variables for a propositional formula was introduced by one of the authors, which made it possible to distinguish the set of hard-determinable formulas. The proof complexity of a formula of this sort has exponential lower bounds in some proof systems of classical propositional calculus (cut-free sequent system, resolution system, analytic tableaux, cutting planes, and bounded Frege systems). In this paper we prove that the property of hard-determinability is insufficient for obtaining a superpolynomial lower bound of proof lines (sizes) in Frege systems: an example of a sequence of hard-determinable formulas is given whose proof complexities are polynomially bounded in every Frege system.     

命题逻辑公式的压缩表示及其相应的形式系统

提出一种将命题逻辑公式压缩表示的方法--公式的压缩图,给出相应的形式系统,并证明该系统的证明效率比传统相继式演算系统Gentzen\{cut}有指数级的提高,从而为命题逻辑提供了一种新的有效的推理系统.