資源描述：
《若干邏輯自動推理方法研究》由會員上傳分享，免費(fèi)在線閱讀，更多相關(guān)內(nèi)容在學(xué)術(shù)論文-天天文庫。
1、華東師范大學(xué)博士學(xué)位論文若干邏輯自動推理方法研究姓名：郭遠(yuǎn)華申請學(xué)位級別：博士專業(yè)：系統(tǒng)分析與集成指導(dǎo)教師：曾振柄20091001摘要自動定理證明(AutomatedTheoremProving)或者機(jī)器定理證明(MechanicalTheoremProving)是通過計(jì)算機(jī)實(shí)現(xiàn)定理證明．二十世紀(jì)五十年代以來自動定理證明一直是計(jì)算機(jī)科學(xué)的熱點(diǎn)之一，在數(shù)學(xué)、硬件測試與驗(yàn)證、軟件生成與驗(yàn)證、協(xié)議驗(yàn)證、人工智能方面都得到了成功的應(yīng)用．部分實(shí)例化方法把一階問題化為一系列命題邏輯中的可滿足性問題來解決一階邏輯的可滿足問題，檢查子句集的滿足式映射中的阻塞是該方法
2、的關(guān)鍵．論文提出的子句搜索方法在判定子旬集可滿足性的同時(shí)給出了一個模型從而得到滿足式映射．格值邏輯的不完全可比性便于描述人類的思維、判斷和決策．格值命題邏輯系統(tǒng)LP(X)于1993年建立，目前對LP(X)系統(tǒng)的自動推理研究主要是歸結(jié)方法，論文討論了它的tableau方法．常用的邏輯證明方法重點(diǎn)在于判定可滿足性而不能給出符合人們閱讀習(xí)慣的演繹過程．歸結(jié)方法、語義表方法、相繼式方法是定理證明中的常用方法，但是重點(diǎn)在于判定而不是演繹，論文探討了相干命題邏輯系統(tǒng)R的試探法實(shí)現(xiàn)和相干自然推理系統(tǒng)NR的自然推理法實(shí)現(xiàn)，生成了類似于手工證明的可讀證明．具體而言論文
3、的工作包括以下幾方面：(1)提出了子旬搜索方法判定命題子句集的可滿足性并給出可滿足子句集的一個模型．子句搜索方法通過查找到子句集①不可擴(kuò)展的子句C來判定①的可滿足性．結(jié)合部分實(shí)例化方法將子句搜索方法提升至一階，分離了謂詞公式的結(jié)構(gòu)和變量，從而提高合一算法的效率并節(jié)省了存貯空間．用正整數(shù)代表原子，負(fù)整數(shù)代表負(fù)文字，簡化了算法實(shí)現(xiàn)．(2)提出了格值命題邏輯系統(tǒng)LP(X)的tableau方法，語義表中的公式都是受限蘊(yùn)涵公式．通過引入Bounds∞、Bounds(X)和極大相容集證明了其正確性和完備性．對于真值域可直積分解的系統(tǒng)三，P(X)，討論了其格直積分
4、解證明．(3)提出了后推試探證明方法并將演繹序列中的各公式組織成證明樹從而產(chǎn)生了類似于手工證明的演繹序列．將公式轉(zhuǎn)化為二叉樹的形式存貯于動態(tài)數(shù)組中減小了公式冗余，用數(shù)組下標(biāo)代表公式簡化了實(shí)現(xiàn)．(4)提出了應(yīng)用于自然推理方法的回溯方法．先從假設(shè)集出發(fā)構(gòu)建證明樹，再從樹根節(jié)點(diǎn)逐層推導(dǎo)各公式的屬性，實(shí)現(xiàn)了相干自然推理系統(tǒng)NR的類似手工證明的自然推理方法證明．綜上所述，論文提出了判定子句集可滿足性的子旬搜索方法并將其提升至一階，提出了格值命題邏輯系統(tǒng)卯∞的tableau方法，提出了后推試探方法和回溯方法并實(shí)現(xiàn)了相干命題邏輯系統(tǒng)尺的可讀證明，在理論和應(yīng)用方面都
5、有積極意義．關(guān)鍵詞：定理證明，自動推理，子句搜索方法，一階邏輯，格值邏輯，tableau方法．試探方法，自然推理方法，可讀證明．AbstractAutomatedtheoremprovingormechanicaltheoremprovingisconcemedwiththebuildingofcomputingsystemsthatautomatetheprocessofprovingtheorems．Sincethe1950sATPhasbeenoneofactiveresearchtopicsofcomputerscienceandsucces
6、sfullyusedinmathematics，hardtestandverification，softwaregenerationandverification，Dro-tocolverification，andartificialintelligence．Thepartialinstantiationmethodreducessatisfiabilityproblemsforfirst-orderlogictoaseriesofground-levelsatisfiabilityproblems．Findingouttheblockagesofs
7、atisfiermappingsforclausesetisnecessaryinthismethod．ClausesearchingmethodproposedbyIISnotonlydecidesthesatisfiabilityofclausesetbutalsopresentsamodelthenob-rainsasatisfiermapping．Lattice—valuedlogicisnotcompletelycomparableandpropertodescribingthinking，judginganddecision—making
8、．Lattice-valuedpropositionallogicsystemLP(X)isproposed
