机器定理证明中的一般问题

木文从人工智能角度阐述了机器定理证明的重要意义,综述了以逻辑方法为重点的定理证明器的一般问题,如搜索策略、化简、语义、抽象、发现相关公理以及它涉及的一般软件工程问题。

基于广义归结的定理机器证明系统

本文使用Ｃ—ＰＲＯＬＯＧ语言在ＳＵＮ工作站上设计实现了基于广义归结和基于归结的两个定理机器证明系统ＧＲＭ，ＲＭ，证明了《数学原理》中Ｐａｒｔ１：ｍａｔｈｅｍａｔｉｃａｌｌｏｇｉｃ中ＳｅｃｔｉｏｎＡ与ＳｅｃｔｉｏｎＢ中全部定理（３５０个）．讨论ＧＲＭ和ＲＭ的时、空复杂性，并在实现设计中提出新的全局调度策略及归结式的化简、排序策略，以单子句恒真、恒假的判断代替了广义归结中的自归结，实现了带ＯＣＣＵＲ检查的模式匹配．

基于Tableau的定理机器证明系统TableauTAP

使用SWI-PROLOG语言在微机上设计实现了基于tableau的定理证明系统TableauTAP。该系统可以证明不含等词的经典逻辑公式和多值逻辑公式,通过预处理自动生成tableau规则,因此容易对其功能进行扩展。应用该系统对TPTP的400个逻辑问题进行证明,实验结果表明,TableauTAP在时间和空间效率上都是比较高的。

从九章消元法到定理机器证明

讨论了《九章算术》中线性代数方程组的解法──九章消元法蕴涵的构造性思想，这一思想后来被进一步发展，并且在某方面影响着定理的机器证明．

定理机器证明的图论法初探

机器定理证明是人工智能的重要分支学科之一 .定理的机器证明已经达到了相当成熟的水平 ,但有关利用图论方法进行定理的机器证明还不多见 .在这样的背景下 ,试图结合机器定理证明的经典方法 ,将图论思想引入进来 ,提出了一种初步的图论机器定理证明方法 ,解决了一类有关定理的机器证明问题 .

定理机器证明与吴文俊方法

作为人类脑力的一种延伸,数学机械化和定理机器证明研究的学术努力及其每一个重大突破,都必将对人类和科学产生意义深远的冲击。

Grobner基方法与吴方法在平面几何定理机器证明中的应用与比较

探讨了在初等平面几何范围内定理机器证明切实可行的2种方法:Grobner基方法与吴方法,介绍了它们相应的算法原理和实现方法,并进行了实践与比较.

机械化数学的典范——评吴文俊的专著《几何定理机器证明的基本原理》

1899年希尔伯特(Hilbert)出版了他的经典名著《几何基础》,从此奠定了几何公理化体系的基础。1984年科学出版社出版的吴文俊的专著《几何定理机器证明的基本原理》(以下简称《原理》)一书,可以说是奠定了几何机械化体系的基础。它可以与《几何基础》媲美,成为机械化数学的典范著作。

改进的几何定理机器证明的概率性算法

将几何定理机器证明的研究方法概括为确定性算法与概率性算法两大类,针对已有的确定性算法和概率性算法的证明速率偏低或占用内存过大等问题,提出一种改进的概率性算法。主要是在改进对多项式中独立变元次数的上界估计的算法的基础上,结合Schwartz-Zippel定理和统计学理论,通过随机检验若干实例来证明几何定理,并能控制证明结果不真的概率在给定的小范围内。通过改进的概率性算法,成功在2秒内证明出代数法难以证明的五圆定理。最后的多组对比实验进一步表明,改进的概率性算法具有明显高效性。

本体推理在几何定理机器证明中的应用

文中阐述了平面几何定理机器证明的基本原理及方法,针对几何定理机器证明过程中可读证明的产生,及推理信息快速增长的问题,提出了一种基于本体推理的几何定理机器证明方法。通过具体案例,描述了以Protégér软件为工具,基于WordNet重用的领域本体半自动构建方法,构建几何本体模型的过程,并结合Prolog规则进行双向推理。结果表明将本体引入几何定理机器证明是可行的,且本体推理脱离了代数形式,使得推理过程更接近自然语言的描述,同时推理效率更高。

集合论等式型定理机器证明系统的研究与开发

集合论定理机器证明,至今在国内外尚无相关研究。虽然集合论在数学领域中所处的基础地位显得在这一领域实现机械化极其重要,但是多年来尚无进展。到目前为止,还没有发现能产生可读证明的系统。通过对人工智能搜索算法的研究,提出了集合论等式型定理证明的机械化方法。实现的系统能自动生成定理的可读证明以及相关的说明。

例证法在定理机器证明中的应用

阐述了例证法的理论 ,分析、论证了例证法应用于定理机器证明的可行性 ,介绍了几何命题代数化的方法和步骤 。

定理的机器证明开创了机械化数学的纪元——《几何定理机器证明的基本原理》评介

《几何定理机器证明的基本原理》一书获第四届全国优秀科技图书奖一等奖。书的著者吴文俊教授是国际知名的数学家,中国科学院学部委员,系统科学研究所的研究员。关于几何定理机器证明是指用计算机证明几何定理,即抛开纸笔,让计算机通过人编制的程序来证明几何定理的成立与否。自远古以来,随着社会的发展与进步,计算已达到了相当高的水平,特别是由于近代计算机的出现,已使机械的计算方法得以充分发挥作用。然而对于证明,虽然早在17世纪莱布尼兹(Leibniz)和笛卡尔(Descartes)

一个古老的梦实现了!——几何定理机器证明的吴法浅谈

我国著名数学家吴文俊教授近年来在几何定理的机器证明方面取得了开创性的成果,他发明的方法被誉为“吴法”。《一个古老的梦实现了!——几何定理机器证明的吴法浅谈》对此作了深入浅出的介绍。

数学定理的机器证明

数学定理的机器证明是中国数学家发展起来的具有中国特色的数学研究新领域,也是我国攀登计划项目之一。项目的核心内容主要是几何定理机器证明和非线性代数方程组理论、算法和应用。能否建立一个通用的几何解题方法、成批地解决问题,以至'万理一证',是历史上一些卓越数学家的梦想。笛卡尔发明了坐标系,莱布尼兹设想过推理机器,希尔伯特、冯·诺伊曼对之作过尝试,但成效甚微。直到1977年,我国数学界的巨星吴文俊教授提出有名的'吴方法',才给定理机器证明的研究带来了生机和活力。什么是数学定理的机器证明呢?

C_m命题演算的定理机器证明系统

C_m系统是制约逻辑的命题演算系统,但是其推导定理的过程可否由图灵(计算机)算法完成尚未得到明确的结论.研究证明了C_m的公式集是递归可枚举集,并且给出了一个递归枚举算法,该算法能够对任一给定的实际可证的C_m式在有限的步骤内判定它属于C_m可证公式集.并给出了C_m命题演算系统的一个定理机器证明系统.因此证明了C_m系统至少是半可判定的.