集合論等式型定理機器證明系統(tǒng)的研究與開發(fā).pdf

1、定理機器證明的研究已有將近50年的歷史，并已經(jīng)在數(shù)理邏輯、初等代數(shù)和幾何學等學科取得顯著成功。關于集合論的定理機器證明研究，有關文獻報道用布爾代數(shù)的方法可以把集合論的定理證明問題轉化為代數(shù)問題，但是這類問題的可讀證明方法，目前尚未查到有關報道。許多國內(nèi)外的著名數(shù)學軟件中，集合論等式型定理的推理方面的功能也比較弱。本論文以人工智能中的搜索算法為基礎，研究集合論等式型定理可讀證明的機械化方法。 本課題所做的工作包括：1、通過比較各種

2、搜索算法，選擇了盲目搜索算法中漸進最優(yōu)的迭代加深算法構建推理樹，并作了必要的改良，以加速搜索路徑的產(chǎn)生。 2、通過研究手工證明和專家經(jīng)驗，總結出幾條啟發(fā)式的規(guī)則引導搜索：根據(jù)使用頻率將公式重新排序；添加了公式反向使用規(guī)則；判斷左右式長短以決定證明方向；分析結果倒序進棧以保證大的匹配結果優(yōu)先擴展。 3、利用編程語言Lisp的特點，尋找了一些適合計算機處理的方法，如推理的內(nèi)部數(shù)據(jù)用前綴形式。 4、使用了一些方法加速調(diào)

3、試，如：先用其他易輸入的半角符號代替難輸入的全角集合運算符，調(diào)通程序；先縮小規(guī)模，驗證程序的執(zhí)行過程；運用注解方便測試與修改；如果真實數(shù)據(jù)過于復雜或難以獲得，第一遍采用仿真數(shù)據(jù)測試，將復雜結果與變量輸出到文件監(jiān)視。 5、采取一些措施，產(chǎn)生詳細推理說明。在每一步代換推理前，記錄所用的規(guī)則以及使用該規(guī)則的理由。 6、通過比較數(shù)理邏輯和集合論相關的規(guī)則，將定理分類推理，基本定理作為經(jīng)驗常識，直接輸出結果，不需要說明，加快了證明