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

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

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

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