若干邏輯自動推理方法研究

1、yiT論女第表超涼若干邏輯自動推理方法研究【摘要】：自動定理證明(AutomatedTheoremProving咸者機器定理證 明(Mecha nicalTheoremProvi ng)是通過計算機實現(xiàn)定理證明.二十世紀 五十年代以來自動定理證明一直是計算機科學的熱點之一，在數(shù)學、硬件測試與驗證、軟件生成與驗證、協(xié)議驗證、人工智能方面都得到 了成功的應(yīng)用部分實例化方法把一階問題化為一系列命題邏輯中的 可滿足性問題來解決一階邏輯的可滿足問題，檢查子句集的滿足式映射中的阻塞是該方法的關(guān)鍵論文提出的子句搜索方法在判定子句集 可滿足性的同時給出了一個模型從而得到滿足式映射格值邏輯的不完全可比性便于描述

2、人類的思維、判斷和決策.格值命題邏輯系統(tǒng)LP(X)于1993年建立，目前對LP(X)系統(tǒng)的自動推理研究主要是歸結(jié) 方法，論文討論了它的tableau方法.常用的邏輯證明方法重點在于判定 可滿足性而不能給出符合人們閱讀習慣的演繹過程歸結(jié)方法、語義表方法、相繼式方法是定理證明中的常用方法，但是重點在于判定而不是演繹，論文探討了相干命題邏輯系統(tǒng)R的試探法實現(xiàn)和相干自然推理系統(tǒng)NR的自然推理法實現(xiàn)，生成了類似于手工證明的可讀證明 具體而言論文的工作包括以下幾方面:(1)提出了子句搜索方法判定命 題子句集的可滿足性并給出可滿足子句集的一個模型子句搜索方法通過查找到子句集不可擴展的子句C來判定的可滿足性結(jié)

3、合部 分實例化方法將子句搜索方法提升至一階，分離了謂詞公式的結(jié)構(gòu)和 變量，從而提高合一算法的效率并節(jié)省了存貯空間用正整數(shù)代表原子負整數(shù)代表負文字，簡化了算法實現(xiàn).(2)提出了格值命題邏輯系統(tǒng) LP(X)的tableau方法,語義表中的公式都是受限蘊涵公式通過引入Bounds(X)、Bound_s(X)和極大相容集證明了其正確性和完備性.對 于真值域可直積分解的系統(tǒng) LP(X),討論了其格直積分解證明.(3)提出 了后推試探證明方法并將演繹序列中的各公式組織成證明樹從而產(chǎn) 生了類似于手工證明的演繹序列將公式轉(zhuǎn)化為二叉樹的形式存貯于 動態(tài)數(shù)組中減小了公式冗余，用數(shù)組下標代表公式簡化了實現(xiàn).(4)提

4、 出了應(yīng)用于自然推理方法的回溯方法先從假設(shè)集出發(fā)構(gòu)建證明樹，再 從樹根節(jié)點逐層推導各公式的屬性，實現(xiàn)了相干自然推理系統(tǒng) NR的 類似手工證明的自然推理方法證明綜上所述，論文提出了判定子句集 可滿足性的子句搜索方法并將其提升至一階，提出了格值命題邏輯系 統(tǒng)LP(X)的tableau方法,提出了后推試探方法和回溯方法并實現(xiàn)了相 干命題邏輯系統(tǒng)R的可讀證明，在理論和應(yīng)用方面都有積極意義.【關(guān) 鍵詞】：定理證明自動推理子句搜索方法一階邏輯格值邏輯tableau方法試探方法自然推理方法可讀證明【學位授予單位】：華東師范大學【學位級別】：博士【學位授予年份】：2010【分類號】：TP181yiT 論女第表

5、&彖【目錄】：摘要6-7Abstract7-10第一章緒論10-181.1自動推理的發(fā)展 簡史10-141.2非經(jīng)典邏輯研究概況14-151.3論文的選題和主要工作15-18第二章一階子句搜索方法18-482.1子句搜索方法18-242.2 一階 子句搜索方法24-462.3本章小結(jié)46-48第三章格值命題邏輯LP(X)的 自動證明 48-683.1基礎(chǔ)知識 48-553.2LP(X)的tableau方法 55-613.3LP(X)的直積分解61-663.4本章小結(jié)66-68第四章相干命題邏 輯R的可讀證明68-1024.1試探法自動證明68-804.2自然推理法自動 證明80-974.3試探法和自然推理法的混合求證 97-1004.4本章小結(jié)