定理證明器是用于證明數(shù)學(xué)定理的正確性的計算機程序。進(jìn)幾十年來,對計算機硬件、軟件形式化驗證等日益增長的需求使得大量形式化工具涌現(xiàn)出來。定理證明器是一種重要的形式化工具,對它們的研究具有重要的意義。目前國內(nèi)在這個方面的研究還比較少。本文設(shè)計并實現(xiàn)了一個基于相繼式演算的一階邏輯定理證明器FolProver,可用于證明一階邏輯中定理的正確性。本文首先對一階邏輯、相繼式演算等理論進(jìn)行了詳細(xì)的分析和論述,包括-階邏輯的語法和語義、相繼式演算的推理規(guī)則及其可靠性完備性等。然后,本文對FolProver進(jìn)行了初步的設(shè)計,按照功能劃分為七個子模塊,并闡明了FolProver的證明機制。接著,本文使用F#和WPF對組成FolProver的各個模塊分別進(jìn)行了具體的設(shè)計和實現(xiàn)。實現(xiàn)的模塊主要包括詞法分析和語法分析、基本推理規(guī)則等模塊。最后,本文以若干具體的問題為例,對FolProver做了實驗演示。實驗結(jié)果表明FolProver在可用性與易用性上表現(xiàn)較好。本文實現(xiàn)的定理證明器FolProver具有圖形界面,支持交互式證明和自動化證明,并具備保存和加載證明等多個便于使用的功能。未來可以在本文的基礎(chǔ)上實現(xiàn)對多種... 

【文章來源】：浙江大學(xué)浙江省 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：90 頁

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

【部分圖文】：

圖４．１１定理證明器ＦｏｌＰｒｏｖｅｒ的用戶界面設(shè)計??回到Ｆ護源代碼中，可Ｗ吏用Ａｐｐｌｉｃａｔｉｏｎ類的ＬｏａｄＣｏｍｐｏｎｅｎｔ方法加載Ｘａｍｌ??文件，并使用巧ｎｄＮａｍｅ方法提�。兀幔恚熘械目丶�

進(jìn)行可視化操作（比如剪除證明樹中的某棵子樹）。在Ｐｒｏｏｆ?Ｔｒｅｅ?Ｖｉｅｗ中顯示證??明樹需要在底層有數(shù)據(jù)作支撐。??證明樹類型定義如圖４．１２所示：??ｔｙｐｅ?Ｔｒｅｅ?二??：Ｎｏｄ？?ｏｆ?Ｓｅｑｕｅｎｔ；參?ｓｔｒｉａ賓?ｒｅｆ?療?ｌｉｓｔ＜Ｔｒ０巧＞?ｒｅｆ??ｉ?Ｅｍｐｔｙ?ｏｆ?泛ｔｒｉｎ沒??團４．１２證明樹的實現(xiàn)??其中，Ｎｏｄｅ是證明樹中的結(jié)點。Ｓｅｑｕｅｎｔ類型的參數(shù)為結(jié)點中的目標(biāo)相繼式，??ｓｔｒｉｎｇ?ｒｅｆ類型的參數(shù)為應(yīng)用在相繼式上的推理規(guī)則的名稱，ｌｉｓｔ＜Ｔｒｅｅ＞?ｒｅｆ類型的??參數(shù)為該結(jié)點所有的子樹。Ｅｍｐｔｙ表示空樹。??除了定義證明樹類型，還需要實現(xiàn)如下函數(shù)；??？為證明樹中的指定葉子結(jié)點插入子樹（當(dāng)執(zhí)行一條推理規(guī)則生成新的目??標(biāo)相繼式時調(diào)用）??？遍歷證明樹，獲取所有的葉子結(jié)點，即獲取當(dāng)前所有待證明的目標(biāo)相繼??式??？刪除證明樹中Ｗ給定相繼式為根的子樹??？在證明樹中搜索某個給定的目標(biāo)相繼式??在Ｐｒｏｖｅｒ模塊中，定義一個Ｔｒｅｅ類型的變量ｃｕｒｒＰｒｏｏｆＴｒｅｅ表示當(dāng)前的證明??樹。當(dāng)開始一個新的證明時，初始化ｃｕｒｒＰｒｏｏｆＴｒｅｅ；當(dāng)在某個待證明的目標(biāo)相繼??式上應(yīng)用指定的推理規(guī)則時，則更新ｃｕｒｒＰｒｏｏｆＴｒｅｅ。當(dāng)要剪除證明樹中Ｗ給定相??繼式為根的某棵子樹時

稱一個集合Ｓ是循環(huán)的（ｃｉｒｃｕｌａｒ），如果Ｓ是另外一個集合ｙ是Ｓ的兒索。直觀上米看，所有的集合都是非循環(huán)集合（ｎｏｎｃｉｒｃｕ選擇一些非循環(huán)集合構(gòu)成一個新的集合。但是，并不存在這樣構(gòu)成的集合。??邏輯無法表示集合的概念，這里仍然選捧使用謂詞來表示上述．ｖ）表示Ｘ是的一個元素，其中Ｘ和ｙ均為集合。＂不存在一成的集合＂可＾＾＾形式化表示為：??－ｉ（３ｙＶｘ（Ｍ（ｘ，ｙ）?＾?－ｉ（３ｚＭ（ｘ，?ｚ）?Ａ?Ｍ（ｚ，?ｘ））））?公使用ＦｏｌＰｒｏｖｅｒ來證明這個定理。按照ＦｏｌＰｒｏｖｅｒ的文法約定，－ｉ（３ｙ．?Ｖｘ．?（Ｍ（ｘ，ｙ）?－ｉ（３ｚ．?Ｍ（ｘ，ｚ）八?Ｍ（ｚ，?ｘ）Ｗ）??目前實現(xiàn)的自動化證明策略，ＦｏｌＰｒｏｖｅｒ無法在有限的時間內(nèi)對化證明，但是可Ｗ交互式地采用更靈活的策略逐步完成對該定每一步使用的推理規(guī)則如圖５．２所示：??

【參考文獻(xiàn)】：
期刊論文
[1]INCAPS:一個交互式計算機輔助定理證明系統(tǒng)[J]. 黎仁蔚.  計算機學(xué)報. 1989(12)

博士論文
[1]用于指針邏輯的自動定理證明器的設(shè)計與實現(xiàn)[D]. 王振明.中國科學(xué)技術(shù)大學(xué) 2009



本文編號：3420991