資源描述：
《探析基于格蘊涵代數的廣義格值模態(tài)邏輯及其歸結自動推理的研究》由會員上傳分享，免費在線閱讀，更多相關內容在學術論文-天天文庫。
1、西南交通大學博士學位論文基于格蘊涵代數的廣義格值模態(tài)邏輯及其歸結自動推理的研究姓名：李文江申請學位級別：博士專業(yè)：交通信息工程及控制指導教師：徐揚20021201西南交通大學博士研究生學位論文第iT摘要格是一類重要的代數結構，現實世界中的很多現象都可以用格來刻畫，尤其是不可比較性。而建立在格上的格值邏輯系統(tǒng)把己有多值邏輯的鏈狀真值域拓展到較一般的格上，既能處理全序性信息，又能處理非全序性信息，從而更有效地描述人類推理、判斷和決策的不確定性。廣義模態(tài)邏輯屬哲學邏輯范疇，對于刻畫事物的“勢態(tài)”、人物的“情態(tài)”和過程的“時態(tài)”是一種十分有效的工具。本文在格值命題邏輯系統(tǒng)LP
2、(X)和格值一階邏輯系統(tǒng)LF(X)的基礎上，討論了廣義格值模態(tài)邏輯系統(tǒng)的語義及語法性質，并對其a一歸結原理做了初步探討，主要在下述三個方面取得了研究成果:第一部分:關于格值模態(tài)命題邏輯系統(tǒng)及其歸結方法的研究在此部分，把模態(tài)算子N(必然)和P(可能)引入格值命題邏輯系統(tǒng)LP(X)，建立了新的格值模態(tài)命題邏輯系統(tǒng)LMP(X)，并研究了它的語義刻畫及語法結構，證明了在此語義解釋和語法框架下的系統(tǒng)仍是a一可靠的和協(xié)調的:在此基礎上，進一步研究了基于格值模態(tài)命題邏輯系統(tǒng)LMP(X)的a一歸結原理，給出了計算a一直接歸結式和a一自歸結式的規(guī)則，并總結出具體的歸結方法.第二部分:關
3、于格值時態(tài)命題邏輯系統(tǒng)及其歸結方法的研究此部分的主要工作是在格值命題邏輯系統(tǒng)LP(X)中引進時態(tài)算子E(曾經)、F(將會)及其對偶算子H(曾經總是)、G(將會總是)，提出了以時軸為語境的格值時態(tài)命題邏輯系統(tǒng)LTP(X)，并給出其具體的語義解釋和語法結構，并討論了它的一些性質，證明了該系統(tǒng)的可靠性和協(xié)調性。此外，研究了與時間有關的(a,t卜歸結原理，給出了計算時態(tài)歸結式的規(guī)則，并提出了時態(tài)歸結的具體方法第三部分:關于格值模態(tài)一階邏輯系統(tǒng)及其歸結原理的研究第ii頁西南交通大學博士研究生學位論文這一部分主要是在格值模態(tài)命題邏輯系統(tǒng)LMP(X)中引進量詞和謂詞，建立格值模態(tài)一
4、階邏輯系統(tǒng)LMF(X)，并給出其語義解釋和語法結構，證明了系統(tǒng)的可靠性和協(xié)調性;另外，為了判斷公式的可滿足性，‘定義了格值模態(tài)一階公式的Skolem標準型和H-解釋;在此基礎上，對基于系統(tǒng)LMF(X)的a一歸結原理進行了初步探討.〔關鍵詞〕格蘊涵代數廣義格值模態(tài)邏輯定理自動證明歸結原理西南交通大學博士研究生學位論文第iii頁AbstractThelaticeisakindofimportantalgebraicstructure.Inourlife,manyphenomenacanbedescribedbylatice,especiallynon-comparabil
5、ity.Latice-valuedlogicsystembasedonlaticeextendslinearvaluedfieldofmulti-valuedlogictolatice,thusnotonlycandealwithorderinformation,butalsocandealwithnon-orderinformation,consequentlydescribetheuncertaintyofhumanreasoning,judginganddecision-makingmoreefectively.Generalizedmodallogicbelo
6、ngstophilosophylogiccategory.Itisaveryefectivetooltodescribethetendencyofthings,atitudeofpeopleandtenseofcourse.Basedonlattice-valuedpropositionallogicsystemLP(X)andlatice-valuedfirst-orderlogicsystemLF(X),theauthorstudiedsemanticandsyntaxpropertiesofgeneralizedlatice-valuedmodallogicsy
7、stem,andprobedintoa一resolutionprinciple.Thespecificcontentsareasfollows:PartOneTheStudyofLattice-valuedModalPropositionalLogicSystemandItsResolutionMethodInthispart,weintroducedmodaloperatorsN(necessary)andP(possible)intolattice-valuedpropositionallogicsystemLP(X),setupanewlatt
