若干邏輯自動(dòng)推理方法研究.pdf

1、自動(dòng)定理證明(Automated Theorem Proving)或者機(jī)器定理證明(MechanicalTheorem Proving)是通過計(jì)算機(jī)實(shí)現(xiàn)定理證明.二十世紀(jì)五十年代以來自動(dòng)定理證明一直是計(jì)算機(jī)科學(xué)的熱點(diǎn)之一，在數(shù)學(xué)、硬件測(cè)試與驗(yàn)證、軟件生成與驗(yàn)證、協(xié)議驗(yàn)證、人工智能方面都得到了成功的應(yīng)用。
　　 部分實(shí)例化方法把一階問題化為一系列命題邏輯中的可滿足性問題來解決一階邏輯的可滿足問題，檢查子句集的滿足式映射中的阻塞是該

2、方法的關(guān)鍵.論文提出的子句搜索方法在判定子句集可滿足性的同時(shí)給出了一個(gè)模型從而得到滿足式映射.格值邏輯的不完全可比性便于描述人類的思維、判斷和決策，格值命題邏輯系統(tǒng)LP(X)于1993年建立，目前對(duì)LP(X)系統(tǒng)的自動(dòng)推理研究主要是歸結(jié)方法，論文討論了它的tableau方法.常用的邏輯證明方法重點(diǎn)在于判定可滿足性而不能給出符合人們閱讀習(xí)慣的演繹過程，歸結(jié)方法、語義表方法、相繼式方法是定理證明中的常用方法，但是重點(diǎn)在于判定而不是演繹，論文

3、探討了相干命題邏輯系統(tǒng)R的試探法實(shí)現(xiàn)和相干自然推理系統(tǒng)NR的自然推理法實(shí)現(xiàn)，生成了類似于手工證明的可讀證明.具體而言論文的工作包括以下幾方面：
　　 (1)提出了子句搜索方法判定命題子句集的可滿足性并給出可滿足子句集的一個(gè)模型.子句搜索方法通過查找到子句集φ不可擴(kuò)展的子句C來判定φ的可滿足性.結(jié)合部分實(shí)例化方法將子句搜索方法提升至一階，分離了謂詞公式的結(jié)構(gòu)和變量，從而提高合一算法的效率并節(jié)省了存貯空間.用正整數(shù)代表原子，負(fù)整數(shù)代

4、表負(fù)文字，簡(jiǎn)化了算法實(shí)現(xiàn)。
　　 (2)提出了格值命題邏輯系統(tǒng)LP(X)的tableau方法，語義表中的公式都是受限蘊(yùn)涵公式.通過引入Bounds(X)、Bounds(X)和極大相容集證明了其正確性和完備性.對(duì)于真值域可直積分解的系統(tǒng)LP(X)，討論了其格直積分解證明。
　　 (3)提出了后推試探證明方法并將演繹序列中的各公式組織成證明樹從而產(chǎn)生了類似于手工證明的演繹序列.將公式轉(zhuǎn)化為二叉樹的形式存貯于動(dòng)態(tài)數(shù)組中減小了公

5、式冗余，用數(shù)組下標(biāo)代表公式簡(jiǎn)化了實(shí)現(xiàn)。
　　 (4)提出了應(yīng)用于自然推理方法的回溯方法.先從假設(shè)集出發(fā)構(gòu)建證明樹，再從樹根節(jié)點(diǎn)逐層推導(dǎo)各公式的屬性，實(shí)現(xiàn)了相干自然推理系統(tǒng)NR的類似手工證明的自然推理方法證明，
　　 綜上所述，論文提出了判定子句集可滿足性的子句搜索方法并將其提升至一階，提出了格值命題邏輯系統(tǒng)LP(X)的tableau方法，提出了后推試探方法和回溯方法并實(shí)現(xiàn)了相干命題邏輯系統(tǒng)R的可讀證明，在理論和應(yīng)用方面都