基于辅助证明程序Coq的不等式的机器证明

发布时间：2021-06-01 07:05

　　随着人工智能技术的发展,数学机械化在计算机与数学交叉领域的影响越来越显著。机器证明是数学机械化领域的重要研究方向之一,指借助计算机和辅助证明程序实现定理的证明。Coq是现在国际上主流的辅助证明程序,它基于归纳构造演算的基本理论,具备严谨性与可靠性的特点。同时,Coq交互式的证明环境增强了代码的可读性。目前,Coq已被广泛应用于各类数学问题的机器证明,尤其是Gonthier和Werner在2005年利用Coq实现了著名的“四色定理”的计算机证明,增强了 Coq在学术界的影响。不等式是数学领域的重要研究课题,几乎所有数学分支学科都离不开不等式。对不等式机器证明的研究,具有普遍的应用价值。近年来不断有新成果涌现,基于数学软件Mathmatica、Maple研发的通用程序已能够机器证明某些不等式,借助辅助证明程序Coq、Isabelle、HOLLight等也实现了对一些不等式的机器证明。本文借助辅助证明程序Coq,给出了算术几何调和平均不等式、Cauchy不等式、排序不等式、Chebyshev不等式、Bernouli不等式、三角不等式和Jensen不等式这七类常用基本不等式的机器证明方法。应该... 

【文章来源】：北京邮电大学北京市 211工程院校 教育部直属院校

【文章页数】：77 页

【学位级别】：硕士

【部分图文】：

Cauchy不等式C}证明过程中的截图

证明“乱序和彡逆序和”。构造两组有序的实数数列Ｓ?ａ２?Ｓ…Ｓ??ａｒｉ和Ｓ?＿１＾２?Ｓ…Ｓ?—ｂｎ，对其应用已完成证明的“顺序和多乱序和”，即（３．３．２）??式，可以直接得证。??小结：??排序不等式的证明分为证明命题“顺序和多乱序和”和“乱序和彡逆序和”??这两步，后者可由前者得到。我们将证明命题“顺序和彡乱序和”转化为证明命??题（３．３．４），并借助Ｃｏｑ分２个步骤完成了这一命题的机器证明，进而排序不等??式成立。??可以看到，排序不等式的整个机器证明过程非常简单。但为了体现辅助证明??程序Ｃｏｑ在常用不等式的机器证明问题的实用性和普遍适用性特点，因此将此??类不等式的形式化机器证明过程也在此描述出来。??

子命题２的证明：??再证明（３．４．４）式，对ｎ进行数学归纳，ｎ?＝?ｌ时显然成立，因此只需证明??命题（３．４．８）成立。同样地，将命题中的？＋ｉ』ｎ＋ｉ??分别用ｒ，ｓ，ｄｙ来表示。由均和单调的性质，最终可以得到命题（３．４．８）。??ｒｓ?＞?ｎｔ，?ｎｘ?＞ｒ，?ｓ?＞?ｎｙ??（ｒ?＋?ｘ）（ｓ?＋?ｙ）?＞?（ｎ?＋?ｌ）（ｔ?＋?ｘｙ）?（３．４．８）??下面将结合Ｃｏｑ代码详细阐述如何借助辅助证明程序Ｃｏｑ实现对这一命题??的形式化描述和机器证明过程。??最开始需要引入Ｒｅａｌｓ和Ｒｅａｌｓｊｎｅｑｕａｔｉｏｎ包，并打开实数辖域Ｒ＿ｓｃｏｐｅ：??Ｒｅｑｕｉｒｅ?Ｉｍｐｏｒｔ?Ｒｅａｌｓ．??Ｒｅｑｕｉｒｅ?Ｅｘｐｏｒｔ?Ｒｅａｌｓ＿ｉｎｅｑｕａｔｉｏｎ．??Ｏｐｅｎ?Ｓｃｏｐｅ?Ｒ＿ｓｃｏｐｅ．??用Ｃｏｑ对命题（３．４．８）进行形式化描述的代码如下：??Ｔｈｅｏｒｅｍ?Ｉｎｅｕａｌｉｔ４＿２??

【参考文献】：
期刊论文
[1]常用基本不等式的机器证明[J]. 杨路,郁文生.  智能系统学报. 2011(05)
[2]一类积分不等式的机器判定[J]. 杨路,郁文生,袁如意.  中国科学:信息科学. 2011(01)
[3]差分代换矩阵与多项式的非负性判定[J]. 杨路,姚勇.  系统科学与数学. 2009(09)
[4]几何定理机器证明三十年[J]. 张景中,李永彬.  系统科学与数学. 2009(09)
[5]数学机械化研究回顾与展望[J]. 吴文俊.  系统科学与数学. 2008(08)
[6]Tarski模型外的一类机器可判定问题[J]. 杨路,姚勇,冯勇.  中国科学（A辑:数学）. 2007(05)
[7]差分代换与不等式机器证明[J]. 杨路.  广州大学学报(自然科学版). 2006(02)
[8]计算机怎样证明几何不等式[J]. 杨路.  广州大学学报(自然科学版). 2004(02)
[9]一类构造性几何不等式的机器证明[J]. 杨路,夏时洪.  计算机学报. 2003(07)
[10]计算机时代的脑力劳动机械化与数学机械化[J]. 吴文俊.  黑龙江大学自然科学学报. 2003(02)



本文编号：3209905