计算机证明：数学黑洞6174

计算机科学的一个重要分支是机器证明,即用计算机来证明代数、几何、图论、物理、化学等不同学科的猜想、定理、公式.其真实意义不在于证明已知的东西,而在于证明或帮助人证明人的智力、能力和时间所不敢问津的问题,举世闻名的“四色定理”就是这样证明出来的.本文尝试证明一个颇具趣味性的题目:卡普雷卡尔常数——数学黑洞6174.《参考消息》1993.3.14～17日,曾连载了关于数学黑洞的文章,1993.7期《读者》杂志又作了摘登,其中一个是6174.这里进一步描述如下:人们都知道,太空中有黑洞.任何物质,一旦掉进了这个黑洞,就永远也出不来了.自然数中也有黑洞.一个任意的四位正整数(数字全相同的除外),将数字重新组合成一个最大的数和一个最小的数,相减,重复这个过程,最多七步,必将得到6174.如1435:5431-1345=4086 8640-0468=81728721-1278=7443 7443-3447=39969963-3699=6264 6642-2466=41767641-1467=6174一日得到6174.“7641-1467=6174”就永远也出不来     

数学机械化问题中的向量加工

1.多项式算法 数学机械化必须首先解决一类数学问题本身的机械化算法问题。作者通过微分方程机械化的实践,并分析了近年来各数学分支领域机械化的结果,认识到这样一个基本事实:相当多一类数学问题的机器定理证明和公式推导,都是对其问题本身寻求代数表示方法,其核心问题最后归结为多项式算法。因此,多项式算法是一个典型的机械化算法。     

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

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

定理证明理论与应用专题前言

<正>随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注.定理证明方法将程序和系统的正确性表达为数学命题,然后使用逻辑推导的方式证明正确性.不同于基于程序测试的技术,定理证明方法能保证覆盖所有边缘情况,完全排除一些特定类型的错误.而基于逻辑推导的交互式定理证明技术还能不受系统状态空间大小和复杂性的限制,验证非常复杂的系统和性质.因此,定理证明技术不仅是形式化方法领域,也是众多其他应用领域国内外学者的关注焦点和研究新热点.近年来,定理证明已经逐步用于越来越多的软件、硬件系统验证,这一方面为软硬件系统的安全性保障提供了新的有力工具,另一方面也成为定理证明技术发展的有利契机.目前,定理证明的规模化问题、定理证明工具本身的底层逻辑理论问题、适应于定理证明方案的程序验证理论问题等变得越来越重要,对于数学分析、离散数学、概率等基础定理证明库或求解方案的需求也越来越迫切.     

代德景问题的机械算法

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

时序逻辑程序的证明系统

本文为时序逻辑语言XYZ/E建立了一个证明系统.其主要特点是:1.证明可以直接在时序逻辑系统中进行,无需另行建立专门的公理系统;2.可建立一些元数学定理以简化证明过程;3.可在逐步求精的过程中边设计边证明正确性.     

基于Z3的Coq自动证明策略的设计和实现

形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高,而使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.本文结合上述两种方式的优点,在定理证明工具Coq中实现了一个自动证明策略smt4coq,它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题,提高了自动化验证的程度,减轻用户手动验证程序的开销.     

模拟Boyer-Moore定理证明器

SBMTP(Simulate Boyer-Moore Theorem Prover)系统是在IBM-PC-386微机上用GCLISP语言实现的一个定理证明系统。该系统采用的思想方法和理论基础是Boyer-Moore的计算逻辑理论. SBMTP主要由三部分组成:知识库管理部分、定理证明部分及中断恢复部分。 知识库管理部分包括一个基本知识库和一系列知识库构造工具。用户可根据具体问题 灵活地组织自己所需要的知识库,定理证明部分采用启发式方法逐步推演,完成证明。中断恢复部分在证明产生中断的情况下提供了较强的恢复能力,提高了证明效率。     

传名调用演算的二值传递CPS变换

为Plotkin带常数传名调用λ演算定义了一个新的CPS(continuation-passing-style)变换方法.方法基于求值上下文变换,新颖之处在于,每次传递二值给继续而不是常规的一值.先给出二值CPS变换编码,再在此基础上定义CPS语言,最后建立源语言和CPS语言的一一映射关系并证明Plotkin的模拟定理.与Plotkin的工作比较,工作特点在于,给出了一个CPS归约闭语言,该语言中所有继续都可以用函数形式表达,且模拟定理的可靠性和完备性方向证明更为简单.     

模拟Boyer-Moore定理证明器

SBMTP(Simulate Boyer-Moore Theorem Prover)系统是在IBM-PC-386微机上用GCLISP语言实现的一个定理证明系统。该系统采用的思想方法和理论基础是Boyer-Moore的计算逻辑理论. SBMTP主要由三部分组成:知识库管理部分、定理证明部分及中断恢复部分。 知识库管理部分包括一个基本知识库和一系列知识库构造工具。用户可根据具体问题 灵活地组织自己所需要的知识库,定理证明部分采用启发式方法逐步推演,完成证明。中断恢复部分在证明产生中断的情况下提供了较强的恢复能力,提高了证明效率。     

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

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

"四色定理"的计算机验证--2001年度全国计算机软件考试高级程序员级下午试题五评析

1题目分析 "四色定理"的证明,标志着计算机数学时代的来临.人们坚定这样一个信念:电脑永远代替不了人脑;然而,在"四色定理"证明的关键部分,计算机起了实质性的作用,并且这种作用是人力可望而不可及的.随着时间的推移,对计算机定理证明持怀疑态度的人会越来越少.对于本题来说跟定理证明还有天然之别,充其量只能是"四色定理"的验证,"四色定理"的证明是一个相当复杂的过程,这里就不多讨论了,而它的验证要简单得多,是把平面区域图的相邻关系用一个对称二阶[0,1]方阵来表示,经过计算机程序的搜索,把所有可能的着色方案找出来.当然,这里的简单只是相对定理证明而言,其本身还是有一定的难度的.如果考生对题目本身以及相关的拓扑学、图论和计算机回溯算法等不太熟悉的话,解答试题就比较困难了.比如你从来就没有玩过地图着色的游戏,现在要你给世界地图着色,并且只能用四种不同的颜色,这实在不是一件轻松的差事.不过,解决问题的办法还是有的,这就是要看考生的基本功了,这也正是2001年度高级程序员下午试题出题者的目的.     

关于组合结构中的连接条件及其有限元法实现

冯康教授在[1,2]中建立了组合弹性结构的力学模型及其相应的数学理论。在此基础上可以发展有限元法并证明一般性的收敛定理. 本文根据这一理论,对用有限元法分析组合结构提出一个具体的实现方案,主要是讨论连续和离散模型中有关连接条件的问题.     

机器证明的困难所在

机器证明是人工智能的一个重要课题,即用计算机来证明定理,亦称自动证明或定理的机械化证明,其基础是由 Hibert 在1930年奠定的,60多年来历程艰苦,困难在于传统逻辑、三段论、充分条件、同理可证、直觉思维的局限性。如果我们正视这些困难,利用专家系统,机器学习等技术,机器证明将进入一个崭新的局面。     

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

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

人工智能(下)

自动定理证明在致力于编制能够证明数学定理和逻辑定理的程序方面明显地存在有三个重要的课题。首先,AI 研究者们的早期工作曾取得了一些能够证明命题逻辑和中学平面几何中的简单定理的启发式程序。     

GJK算法的一种特殊情形的形式化验证和应用

计算几何算法经常用于机器人避碰运动规划等安全攸关领域,对这些算法进行正确性证明非常重要.用形式化方法对算法进行验证是一种十分有效的手段,尤其是定理证明的方法用严格的数学公理和定理推理证明逻辑模型的性质,对所验证的性质而言是完备的.基于GJK算法设计了计算空间两条线段间距离的算法,用定理证明器HOL4对其相关的定义和定理进行形式化定义和证明,进而基于霍尔逻辑完成形式化表示和证明,对该算法的正确性实现了形式化验证.最后,给出了这一经过验证的算法在双臂机器人无碰撞运动规划中的应用.     

针对教学场景的ZFC集合论Coq形式化

离散数学是计算机类专业的基础课程之一,命题逻辑、一阶逻辑与公理集合论是其重要组成部分.教学实践表明,初学者准确理解语法、语义、推理系统等抽象概念是有一定难度的.近年来,已有一些学者开始在教学中引入交互式定理证明工具,以帮助学生构造形式化证明,更透彻地理解逻辑系统.然而,现有的定理证明器有较高上手门槛,直接使用会增加学生的学习负担.鉴于此,在Coq中开发了针对教学场景的ZFC公理集合论证明器.首先,形式化了一阶逻辑推理系统和ZFC公理集合论;之后,开发了数条自动化推理规则证明策略.学生可以在与教科书风格相同的简洁证明环境中使用自动化证明策略完成定理的形式化证明.该工具被用在了大一新生离散数学课程的教学中,没有定理证明经验的学生使用该工具可以快速完成数学归纳法和皮亚诺算术系统等定理的形式化证明,验证了该工具的实际效果.     

唯一质数因子分解定理

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

哥德巴赫猜想的筛法验证

哥德巴赫猜想:“任何一个大于等于6的偶数,都可以表示为两个奇素数之和”,被誉为“数学皇冠上的明珠”.古今中外,一代又一代卓有成就的天才数学家为证明它而耗尽毕生心血,我国数学家陈景润先生集前人之大成,证明了“1十2”,留下了“陈氏定理”,但也未能攀上“1+1”的顶峰摘下“明珠”,而英年早逝,令世人万分遗憾.数学的发展一直是围绕着证明和构造反例进行的,这是数学进步的两条腿.一个猜想对不对,要么证明它,要么举出一个反例否定它.对于哥德巴赫猜想,想证明它的人已历几代,想用反倒否定它的人可能更多,尤其是计算机问世以后,已经试到天文数了,不满足哥德巴赫猜想的偶数还未找到一个,这就更增加了“明珠”的光辉.