發(fā)布時(shí)間：2021-06-01 07:05

　　隨著人工智能技術(shù)的發(fā)展,數(shù)學(xué)機(jī)械化在計(jì)算機(jī)與數(shù)學(xué)交叉領(lǐng)域的影響越來(lái)越顯著。機(jī)器證明是數(shù)學(xué)機(jī)械化領(lǐng)域的重要研究方向之一,指借助計(jì)算機(jī)和輔助證明程序?qū)崿F(xiàn)定理的證明。Coq是現(xiàn)在國(guó)際上主流的輔助證明程序,它基于歸納構(gòu)造演算的基本理論,具備嚴(yán)謹(jǐn)性與可靠性的特點(diǎn)。同時(shí),Coq交互式的證明環(huán)境增強(qiáng)了代碼的可讀性。目前,Coq已被廣泛應(yīng)用于各類數(shù)學(xué)問(wèn)題的機(jī)器證明,尤其是Gonthier和Werner在2005年利用Coq實(shí)現(xiàn)了著名的“四色定理”的計(jì)算機(jī)證明,增強(qiáng)了 Coq在學(xué)術(shù)界的影響。不等式是數(shù)學(xué)領(lǐng)域的重要研究課題,幾乎所有數(shù)學(xué)分支學(xué)科都離不開不等式。對(duì)不等式機(jī)器證明的研究,具有普遍的應(yīng)用價(jià)值。近年來(lái)不斷有新成果涌現(xiàn),基于數(shù)學(xué)軟件Mathmatica、Maple研發(fā)的通用程序已能夠機(jī)器證明某些不等式,借助輔助證明程序Coq、Isabelle、HOLLight等也實(shí)現(xiàn)了對(duì)一些不等式的機(jī)器證明。本文借助輔助證明程序Coq,給出了算術(shù)幾何調(diào)和平均不等式、Cauchy不等式、排序不等式、Chebyshev不等式、Bernouli不等式、三角不等式和Jensen不等式這七類常用基本不等式的機(jī)器證明方法。應(yīng)該... 

【文章來(lái)源】：北京郵電大學(xué)北京市 211工程院校 教育部直屬院校

【文章頁(yè)數(shù)】：77 頁(yè)

【學(xué)位級(jí)別】：碩士

【部分圖文】：

Cauchy不等式C}證明過(guò)程中的截圖

證明“亂序和彡逆序和”。構(gòu)造兩組有序的實(shí)數(shù)數(shù)列Ｓ?ａ２?Ｓ…Ｓ??ａｒｉ和Ｓ?＿１＾２?Ｓ…Ｓ?—ｂｎ，對(duì)其應(yīng)用已完成證明的“順序和多亂序和”，即（３．３．２）??式，可以直接得證。??小結(jié)：??排序不等式的證明分為證明命題“順序和多亂序和”和“亂序和彡逆序和”??這兩步，后者可由前者得到。我們將證明命題“順序和彡亂序和”轉(zhuǎn)化為證明命??題（３．３．４），并借助Ｃｏｑ分２個(gè)步驟完成了這一命題的機(jī)器證明，進(jìn)而排序不等??式成立。??可以看到，排序不等式的整個(gè)機(jī)器證明過(guò)程非常簡(jiǎn)單。但為了體現(xiàn)輔助證明??程序Ｃｏｑ在常用不等式的機(jī)器證明問(wèn)題的實(shí)用性和普遍適用性特點(diǎn)，因此將此??類不等式的形式化機(jī)器證明過(guò)程也在此描述出來(lái)。??

子命題２的證明：??再證明（３．４．４）式，對(duì)ｎ進(jìn)行數(shù)學(xué)歸納，ｎ?＝?ｌ時(shí)顯然成立，因此只需證明??命題（３．４．８）成立。同樣地，將命題中的？＋ｉ』ｎ＋ｉ??分別用ｒ，ｓ，ｄｙ來(lái)表示。由均和單調(diào)的性質(zhì)，最終可以得到命題（３．４．８）。??ｒｓ?＞?ｎｔ，?ｎｘ?＞ｒ，?ｓ?＞?ｎｙ??（ｒ?＋?ｘ）（ｓ?＋?ｙ）?＞?（ｎ?＋?ｌ）（ｔ?＋?ｘｙ）?（３．４．８）??下面將結(jié)合Ｃｏｑ代碼詳細(xì)闡述如何借助輔助證明程序Ｃｏｑ實(shí)現(xiàn)對(duì)這一命題??的形式化描述和機(jī)器證明過(guò)程。??最開始需要引入Ｒｅａｌｓ和Ｒｅａｌｓｊｎｅｑｕａｔｉｏｎ包，并打開實(shí)數(shù)轄域Ｒ＿ｓｃｏｐｅ：??Ｒｅｑｕｉｒｅ?Ｉｍｐｏｒｔ?Ｒｅａｌｓ．??Ｒｅｑｕｉｒｅ?Ｅｘｐｏｒｔ?Ｒｅａｌｓ＿ｉｎｅｑｕａｔｉｏｎ．??Ｏｐｅｎ?Ｓｃｏｐｅ?Ｒ＿ｓｃｏｐｅ．??用Ｃｏｑ對(duì)命題（３．４．８）進(jìn)行形式化描述的代碼如下：??Ｔｈｅｏｒｅｍ?Ｉｎｅｕａｌｉｔ４＿２??

【參考文獻(xiàn)】：
期刊論文
[1]常用基本不等式的機(jī)器證明[J]. 楊路,郁文生.  智能系統(tǒng)學(xué)報(bào). 2011(05)
[2]一類積分不等式的機(jī)器判定[J]. 楊路,郁文生,袁如意.  中國(guó)科學(xué):信息科學(xué). 2011(01)
[3]差分代換矩陣與多項(xiàng)式的非負(fù)性判定[J]. 楊路,姚勇.  系統(tǒng)科學(xué)與數(shù)學(xué). 2009(09)
[4]幾何定理機(jī)器證明三十年[J]. 張景中,李永彬.  系統(tǒng)科學(xué)與數(shù)學(xué). 2009(09)
[5]數(shù)學(xué)機(jī)械化研究回顧與展望[J]. 吳文俊.  系統(tǒng)科學(xué)與數(shù)學(xué). 2008(08)
[6]Tarski模型外的一類機(jī)器可判定問(wèn)題[J]. 楊路,姚勇,馮勇.  中國(guó)科學(xué)（A輯:數(shù)學(xué)）. 2007(05)
[7]差分代換與不等式機(jī)器證明[J]. 楊路.  廣州大學(xué)學(xué)報(bào)(自然科學(xué)版). 2006(02)
[8]計(jì)算機(jī)怎樣證明幾何不等式[J]. 楊路.  廣州大學(xué)學(xué)報(bào)(自然科學(xué)版). 2004(02)
[9]一類構(gòu)造性幾何不等式的機(jī)器證明[J]. 楊路,夏時(shí)洪.  計(jì)算機(jī)學(xué)報(bào). 2003(07)
[10]計(jì)算機(jī)時(shí)代的腦力勞動(dòng)機(jī)械化與數(shù)學(xué)機(jī)械化[J]. 吳文俊.  黑龍江大學(xué)自然科學(xué)學(xué)報(bào). 2003(02)



本文編號(hào)：3209905