基于Coq的杨忠道定理形式化证明

实现拓扑学定理的机器证明,是吴文俊院士生前的宿愿.杨忠道定理涉及一般拓扑学中的诸多基本概念,对深刻理解拓扑空间的本质有重要意义.该定理表明,拓扑空间中每一个子集的导集为闭集当且仅当此空间中的每一个单点集的导集为闭集,是一般拓扑学中的一个重要定理.基于定理证明辅助工具Coq,从公理化集合论机器证明系统出发,对一般拓扑学中的开集、闭集、邻域、凝聚点和导集等拓扑基本概念进行形式化描述,给出这些概念基本性质的形式化验证,建立了拓扑空间的形式化框架.在此基础上,实现基于Coq的杨忠道定理形式化证明.全部引理、定理和推论均完整给出Coq的形式化描述和机器证明代码,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.杨忠道定理的形式化证明是一般拓扑学形式化内容的一个深刻体现.     

基于复数法的几何定理可读机器证明

已有的机器证明方法在处理一些涉及大规模符号运算的几何问题时,常因算法复杂度过高或机器能力的限制,有时并不能在合理时间内实现可读机器证明.故提出了复数法这一新的几何定理机器证明算法,并选用符号计算功能较为强大的软件Mathematica创建了新证明器CNMP(complex number method prover).新提出的复数法能有效地解决构造型几何命题,对用于测试与评价几何定理证明器性能的综合性平台TGTP(thousands of geometric problems for geometric theorem provers)上的180个几何问题的实验结果表明,CNMP的解题能力与运行效率均令人满意.尤其是对于一些具有相当难度的几何定理,如五圆定理、Morley定理、Lemoine圆定理、Thebault定理、Brocard圆定理等,CNMP均能在短时间内给出可读机器证明.     

基于拼凑替换的定理机器证明的研究与实现

机器定理证明可以避免人工证明容易出现的低级错误,是人工智能的重要方面,有广泛的应用前景;函数式程序设计的设计思想更加接近于数学,在定理证明方面有天然优势.人们证明逻辑推理的过程通过函数式程序实现,并将其证明的步骤显示出来,采用了逻辑推理机器证明.通过思考人脑在证明定理时的思考方式,给出了一个简单易懂的机器证明的方式.首先将证明的已知和结论形式化,将已知设为start,结果为end,已经证明的公理就是road,那么证明的过程就是从start沿着road到达end的过程.实验表明,逻辑证明通过函数式程序实现,达到了预期目的.     

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

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

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

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

定理的机器证明及其实现

定理的机器证明是人工智能近代主攻的课题之一。早在十六世纪,人类就开始考虑这一问题,但由于历史条件的限制没能付诸实践。从本世纪六十年代以来,随着大型高速计算机的发展,人们继前辈之理论,集众人之精华研究出一个个精致的定理的机器证明方法,从而开创了这一学科的新纪元.     

命题演算形式系统在Isabelle／HOL中的形式化

本文针对命题演算形式系统,在机器辅助定理证明系统Isabelle／HOL中为其建立逻辑模型,并分别形式化验证了PC和ND的主要性质,以及完备性定理的证明。通过对PC和ND的分析和验证表明,采用机器辅助定理证明系统,对以数理逻辑为平台的各种形式系统进行严格的分析和证明是可行的。     

代德景问题的机械算法

数学定理的证明是人类演绎能力的最集中表现,能否使数学定理证明机械化,是人工智能中的一个重要课题。六十年代以来,定理的机械证明,引起了人们极大的兴趣[1,2]。由于计算机的计算速度快,许多需要通过大量计算,才能获得其结论的问题,就可以通过计算机的计算,求出部分结果,猜出结论,然后编好程序,让机器进行自动证明。文献[1]对于     

基于演化Agent的推理模型

本文描述了一种基于演化 agent的推理模型 ,并用这种推理模型来处理定理机器证明 .传统上 ,定理机器证明常常使用某种逻辑表示 ,然后再进行推理 ,这些方法往往缺乏灵活性 ,且证明过程难以理解 .在本文所叙述的方法中 ,演化 agent能将目标即待证定理分解成越来越小且越来越容易证明的子目标 ,最后完成定理证明 .这种方法非常类似于人类在证明定理时一般所采用的思维方式 ,因而 ,显得更灵活、更具有适应性     

区间时序逻辑的标记相继式演算

区间逻辑在许多领域如人工智能,形式化方法中都有成功应用。其中,区间时序逻辑及其各种扩充近年来越来越多地受到人们的重视,由于区间时序逻辑具有较强的表达能力,这也使得该逻辑的定理证明变得相当困难,该文提出了区间时序逻辑的一个标记相继式演算,并给出其可靠性和相对完备性结论。该演算应用于机器辅助定理证明工具中,可以有效地提高证明的自动化程度,在高阶逻辑证明了工具ＰＶＳ中,作者尝试性地实现了这一演算,获得了     

几何定理机器证明的强正常升列分解算法

自上个世纪70年代吴文俊的开创性工作以来，几何定理机器证明这个曾被深人研究而停滞不前的分支在自动推理领域变得异常活跃，大量学术论著相继出现。国内外众多学者，如Chou，Koand Hussain，Wangand Gao，Wang，Zhang，Yangand Hou等提出了各种成功的有效的几何定理机器证明算法。这些方法及其变形已由多位学者实施，使用不同的证明器已经获得了大量几何定理的机器证明。这些定理包括(广义)：史坦纳定理；摩勒三分角线定理以及最近确认的泰博猜想。     

出具证明编译器中线性整数命题证明的自动生成

近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助自动定理证明技术,自动地证明验证条件并生成机器可检查的证明项,因此好的自动定理证明器对出具证明编译器至关重要.本文基于Simplex算法在出具证明编译器的框架内设计并实现了一个支持线性整数命题求解的自动定理证明器,并且提出一套证明项构造方法,将其应用于自动定理证明器中可生成Coq可检查的证明.     

OI-归结法的半完备性

本文指出,定理机器证明的OI-归结法是半完备的。     

SGARP中符号计算模块的实现及其应用

可持续发展的几何自动推理平台(sustainable geometry automated reasoning platform,SGARP)支持用户按需添加或修改几何定理机器证明所涉及的几何对象、谓词、定理和规则,以发展多种多样基于规则的机器自动推理或人机交互推理方法.为进一步提高SGARP的推理能力和扩展其适用范围,提出一种在SGARP中实现符号计算功能的快捷方法,并成功添加了质点法和解析法推理模块.质点法可证明希尔伯特交点类几何命题,解析法能用于辅助证明各种类型有一定难度的几何定理,如著名的Thebault定理.对这两种方法用基于Web的机器证明测试用的几何问题库(thousands of geometric problems for geometric theorem provers,TGTP)中180道几何题进行评估,均在合理时间内给出令人满意的可读机器证明,表明升级后的SGARP能更好地满足用户学习与发展几何机器推理的需求.     

在APPLEⅡ机上实现自动定理证明

作者根据锁归结(lock resolution)原理用LISP语言编制了完整的框图和程序,并在APPLE Ⅱ机器上实现了对命题逻辑中的定理的证明。归结原理的证明过程采用了反驳(refutation)的形式,这很像数学中的反证法。为了使一个定理能在计算机上得以证明,首先要把定理的前提和结论都化为逻辑表达式,然后把定     

唯一质数因子分解定理

<正> 本章讨论我们系统对唯一质数因子分解定理的证明,该定理著称为算术的基本定理。它是我们定理证明器所证过的最深最难的定理。证明该定理的主要困难在于Euclid最大公因子函数(GCD)起着重要的作用,尽管它未包含在定理的语句中。证明使用了一个漂亮但令人吃惊的事实(即,乘法在GCD上分配);还使用了两个数的GCD整除那两个数这一更为明显的事实。没有哪条由定理证明器证过的定理把(未在定理的语句中涉及的)有关一函数的惊人事实作为引理。     

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

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

应用本体和AllegroGraph实现几何定理证明

由于传统的定理机器证明方法是基于规则的,使得定理证明出现几何信息增长迅猛,推理和计算效率低以及过程可读性差等问题。针对以上情况,提出了基于本体和AllegroGraph的几何定理证明方法。该方法通过本体构建几何定理命题模型,然后采用Prolog规则描述语言对几何定理性质进行描述,同时通过分析本体模型和规则描述的对应关系,提出定理规则半自动生成方法。最后以AllegroGraph（ AG）图形数据库的推理机制为基础,完成几何定理证明。实验结果表明,将本体和AllegroGraph推理机应用于几何定理证明领域可以摆脱以往几何定理证明代数化问题,几何证明过程容易理解,同时合理地控制了信息的增长,支持定理可持续证明。     

我们是怎样证明定理的

<正> 本章和后十章将描述我们理论中的一些定理证明技术。实际上,就是描述我们的机械定理证明程序是如何工作的。熟悉机械定理证明的读者,根据这些讨论应能重新构造出我们的定理证明器。而不熟悉机械定理证明的读者,跟上我们的介绍也不会感到困难。虽不要求任     

奇妙解题之二:计算机证明:数学黑洞153

计算机科学的一个重要分支是机器证明,即用计算机来证明代数、几何、图论、物理、化学等不同学科的猜想、定理、公式.其真实意义不在于证明已知的东西,而在于证明或帮助人证明人的智力、能力和时间所不敢问津的问题,举世闻名的“四色定理”就是这样证明出来的.本文尝试证明一个颇具趣味性、学术性的问题:数学黑洞153.一、问题的提出人们都知道,太空中有黑洞.任何物质,一旦掉进了这个黑洞,就永远也出不来了.再看数学领域.正整数153,各位数字的立方和仍等于这个数153: