格值一階邏輯系統的α廣義歸結原理

許偉濤,張聞強,徐 揚,張德賢

(1.河南工業大學信息科學與工程學院,河南鄭州 450001; 2.西南交通大學數學學院,四川成都 610031)

格值一階邏輯系統的α廣義歸結原理

許偉濤1,張聞強1,徐 揚2,張德賢1

(1.河南工業大學信息科學與工程學院,河南鄭州 450001; 2.西南交通大學數學學院,四川成都 610031)

在基于格蘊涵代數的格值邏輯系統框架下,筆者擴展了基于格值邏輯系統的α歸結原理,將廣義子句集上的歸結擴展到一般廣義子句集上,提出了基于格值一階邏輯系統LF(X)的α廣義歸結原理,建立了格值一階邏輯系統中α廣義歸結原理的可靠性定理.通過給出的提升引理,證明了該原理的弱完備性定理.這將為建立基于格值邏輯系統的廣義歸結方法提供新的自動推理技術.

格值一階邏輯;一般廣義子句;局部極復雜廣義文字;廣義歸結;自動推理

自動推理是人工智能領域的重要研究內容.基于歸結原理的自動推理是自動推理研究的重要方法. Robinson于1965年提出了基于經典邏輯的歸結原理[1],為基于歸結原理的自動推理提供了重要的研究基礎.之后,自動推理的研究也取得了較多的研究成果[2-9].

基于經典二值邏輯的歸結自動推理理論,已形成各種各樣的歸結自動推理方法,典型的有語義歸結、鎖歸結和線性歸結.這些歸結方法在證明定理時要將定理的否定寫成一階邏輯中的公式,再把公式化成Skolem標準型,然后將標準型的母式化為合取范式,而合取范式中的每一項都是一個子句,把該合取范式對應一個子句集,即只需證明這個子句集是不可滿足的,就相當于完成了該定理的證明[8].為更自然、直觀地對問題描述形成的公式所對應的子句集進行歸結,王湘浩和劉敘華將傳統的歸結原理推廣到廣義子句集上,提出了基于經典二值邏輯的廣義歸結原理[8],使得演繹過程更加接近自然推導.

對確定性問題可以用經典二值邏輯解決,但是在處理含不確定性信息或知識時,問題的解決往往是困難的.為處理帶有不確定性或不可比較性的信息,徐揚結合格和蘊涵代數提出了格蘊涵代數的概念[10],隨后徐揚等建立了基于格蘊涵代數的格值命題邏輯系統LP(X)和格值一階邏輯系統LF(X)[4,11],為基于格值邏輯系統的自動推理提供了良好的邏輯基礎.基于格蘊涵代數的格值邏輯系統,既有邏輯公式的形式演繹,同時又有形式演繹真值的合理傳遞.在格值命題邏輯系統和格值一階邏輯系統框架下徐揚等分別建立了α歸結原理[12-13],也給出了49種情況下廣義文字可歸結性的判定方法[14].

借鑒經典邏輯的廣義歸結原理,徐揚提出了基于格值命題邏輯系統LP(X)的α廣義歸結原理,將廣義子句集推廣到了一般廣義子句集上,使一般廣義子句直接參與歸結過程[15-16].筆者依據以上的研究成果,進一步研究基于格蘊涵代數的格值一階邏輯系統LF(X)的α廣義歸結原理,為建立基于格值邏輯系統的廣義歸結自動推理方法提供基礎.

1 預備知識

格值一階邏輯系統LF(X)指基于格蘊涵代數L=(L,∨,∧,′,→,O,I)的格值一階邏輯系統,格蘊涵代數的概念及主要性質參看文獻[4,10],下面將簡要給出基于格值一階邏輯系統LF(X)的α歸結原理.

定義1 在格值一階邏輯系統LF(X)中,設α∈L,且廣義子句[4]

如果廣義文字gi和hj在替換σ下使得則

稱為C1和C2的α歸結式,記作Rα(C1,C2).(gi,hj)稱為一個α歸結對,記作(gi,hj)-α.

定義2 在格值一階邏輯系統LF(X)中,設S={C1,…,Ci,…,Cn},是一個廣義子句集,α∈L.如果滿足下列條件[4]之一:

(1)Di∈S,

(2)存在j,k＜i,使得Di=Rα(Dj,Dk),

則稱ω={D1,…,Di,…,Dm},是一個從廣義子句集S出發到廣義子句Dm的α歸結演繹.

定理1(α歸結原理的可靠性)[4]設S是格值一階邏輯系統LF(X)的一個廣義子句集,α∈L,ω={D1,…,Di,…,Dm},是一個從S出發到廣義子句Dm的α歸結演繹.如果Dm=α,則S≤α,即如果Dm≤α,則S≤α.

定理2(α歸結原理的弱完備性)[4]設S是格值一階邏輯系統LF(X)的一個廣義子句集,S*是廣義子句集S的廣義Skolem標準型,α∈L,α＜I.如果S*≤α,則存在一個從S*出發到α的α歸結演繹.

定義3 在格值命題邏輯系統LP(X)中,設C是一個廣義子句,g是廣義文字,A(C)和A(g)分別是C和g的原子集.如果A(C)∩A(g)=?,則稱C和g是相互獨立的[16].

定義4 在格值命題邏輯系統LP(X)中,g是一個廣義文字.如果存在一個賦值v使得v(g)=I,則稱g是正規的[16].

格值邏輯系統、基于格值邏輯系統的α歸結原理的詳細內容參看文獻[4].

2 基于格值一階邏輯系統LF(X)的α廣義歸結原理

這一節將推廣基于格值一階邏輯系統LF(X)的α歸結原理,給出LF(X)中一般廣義子句的概念,并提出基于格蘊涵代數L的格值一階邏輯系統LF(X)的α廣義歸結原理.

定義5 設g1,g2,…,gn是格值一階邏輯系統LF(X)中的廣義文字,Φ(g1,g2,…,gn)是由邏輯聯結詞“∨,∧,′,→,?”連接這些廣義文字構成的一個格值邏輯公式,則稱這個邏輯公式是LF(X)中的一般廣義子句.

例1 設LF(X)是基于格蘊涵代數L的格值一階邏輯系統,則

是一般廣義子句,這里,a∈L,p,q,r是關系符號,x,y,z是個體變元.

根據格值一階邏輯系統LF(X)中對公式的語義解釋,給出一般廣義子句作為一個格值邏輯公式的α可滿足性、α真和α假的定義.

定義6 設Φ是格值一階邏輯系統LF(X)中的一般廣義子句,α∈L,α＜I.

(1)如果存在解釋ID=,有vD(Φ)＞α,則稱Φ是α可滿足.

(2)如果對任意的解釋ID=,有vD(Φ)＞α,則稱Φ是α真.

(3)如果對任意的解釋ID=,有vD(Φ)≤α,則稱Φ是α假.

對于一個格值邏輯公式,如果含有存在量詞或廣義量詞,可以借助于下面定理對該公式進行等價變形.

定理3 在格值一階邏輯系統LF(X)中,設Φ和Ψ是格值邏輯公式,x不是Φ中的自由變元,則下列結論成立:

(1)Φ→(?x)Ψ=(?x)(Φ→Ψ),Φ→(?x)Ψ=(?x)(Φ→Ψ).

(2)(?x)Ψ→Φ=(?x)(Ψ→Φ),(?x)Ψ→Φ=(?x)(Ψ→Φ).

(3)Φ∨(?x)Ψ=(?x)(Φ∨Ψ),Φ∧(?x)Ψ=(?x)(Φ∧Ψ).

(4)Φ∨(?x)Ψ=(?x)(Φ∨Ψ),Φ∧(?x)Ψ=(?x)(Φ∧Ψ).

在格值一階邏輯系統LF(X)中,設S=Φ1∧…∧Φi∧…∧Φn,Φi(i=1,2,…,n)是一般廣義子句,則稱S為一般廣義子句集,記作S={Φ1,…,Φi,…,Φn}.

定義7 設S是格值一階邏輯系統LF(X)中的一般廣義子句集,x1,x2,…,xn是S中的所有自由變元,則邏輯公式?x1?x2…?xnS*稱為S的格值全稱化,即,邏輯公式?x1?x2…?xnS*稱為S的格值全稱封閉公式.

特別地,如果邏輯公式S中沒有自由變元,則S的格值全稱封閉公式為S本身.

下面所提到的格值一階邏輯系統LF(X)中的一般廣義子句集都是指一個格值全稱封閉公式.

定義8 設Φ是格值一階邏輯系統LF(X)中的一般廣義子句,如果某些局部極復雜廣義文字gi(i=1,2,…,r)存在一個最一般合一σ,則稱Φσ是Φ的一個因子.

定義9 設Φ(g1,g2,…,gi,…,gn)和Ψ(h1,h2,…,hj,…,hn)是格值一階邏輯系統LF(X)中兩個沒有公共變元的一般廣義子句,α∈L.如果存在最一般合一σ、τ和替換ρ滿足條件:

(1)Φσ是通過合一Φ中局部極復雜廣義文字gi1,gi2,…,gis的因子,

(2)Ψτ是通過合一Ψ中局部極復雜廣義文字hj1,hj2,…,hjs的因子,

為了得到α廣義歸結原理的可靠性定理,先給出下面一個定理,即廣義歸結式是兩個一般廣義子句的邏輯結果.

定理4 設Φ和Ψ是格值一階邏輯系統LF(X)中的兩個一般廣義子句,α∈L,α＜I.如果在Φ和Ψ中分別存在局部極復雜廣義文字g和h在替換ρ下滿足gρ∧hρ≤α,且Rf(α-g)-g(Φ,Ψ)是Φ和Ψ的α廣義歸結式,則

證明 因為在Φ和Ψ中分別存在局部極復雜廣義文字g和h在替換ρ下滿足gρ∧hρ≤α,根據文獻[16]中的定理3.1,則Φρ∧Ψρ≤Φρ(gρ=α)∨Ψρ(hρ=α).

而Φ∧Ψ≤Φρ∧Ψρ,所以,Φ∧Ψ≤Φρ(gρ=α)∨Ψρ(hρ=α).

定義10 設S是格值一階邏輯系統LF(X)中的一般廣義子句集,α∈L,α＜I.ω={D1,…,Di,…,Dm},是從廣義子句集S出發到一般廣義子句Dm的一個α廣義歸結演繹,如果滿足

(1)Di∈S,或者

下文給出基于格值一階邏輯系統LF(X)的α廣義歸結原理的可靠性,同時建立提升引理,給出該原理的弱完備性定理.

定理5(可靠性) 設S是格值一階邏輯系統LF(X)中的一般廣義子句集,α∈L,α＜I.ω={D1,…,Di,…,Dm},是從廣義子句集S出發到一般廣義子句Dm的一個α廣義歸結演繹.如果Dm是α″,則S≤α,即Dm≤α,則S≤α.

證明 根據定理4容易得到.證畢.

證明 設Φ1和Φ2是LF(X)中的兩個一般廣義子句.如果Φ1和Φ2中沒有公共變元,則分別設為x1,x2,…,xn和y1,y2,…,yn;否則重新命名Φ1和Φ2中的變元,使得它們沒有公共變元.假設Φ1和Φ2中已經沒有公共變元.

圖1 α廣義歸結原理的提升引理

(2)Φ1=Φ1(g1,g11,g12,…,g1r1)滿足條件{g1,g11,g12,…,g1r1}={h|h是Φ1中的局部極復雜廣義文字,},Φ2=Φ2(g2,g21,g22,…,g2r2)滿足條件{g2,g21,g22,…,g2r2}={h|h是Φ2中的局部極復雜廣義文字,.于是,其中,Φ1(g1,g11,g12,…,g1r1)表示在Φ1中的局部極復雜廣義文字g1,g11,g12,…,g1r1是可以合一的表示將g1,g11,g12,…,g1r2合一為后得到的一般廣義子句.Φ2=Φ2(g2,g21,g22,…,g2r2)表示在Φ2中的局部極復雜廣義文字g2,g21,g22,…,g2r2是可以合一的.表示將g1,g11,g12,…,g1r2合一為后得到的一般廣義子句.

定理7(弱完備性) 設S是格值一階邏輯系統LF(X)中的一般廣義子句集,α∈L,α＜I,HS={g1,g2,…,gn},是S中一般廣義子句的局部極復雜廣義文字集合.如果滿足下列條件:

(1)S≤α,

(2)h1和h2分別是一般廣義子句Φ和Ψ中的局部極復雜廣義文字,使得在替換ρ下有hρ1∧hρ2≤α,且和分別與一般廣義子句集Sρ*是相互獨立的,其中,則存在一個從一般廣義子句集S出發到α的α廣義歸結演繹.

證明 如果一般廣義子句集S≤α,根據文獻[4]中的定理11.4.5,則存在一般廣義子句集S的一個有限基例集S0,使得S0≤α.通過文獻[16]中的定理3.3,存在從一般廣義子句集S0出發到α的α廣義歸結演繹ω0.根據定理6和α廣義歸結演繹ω0,存在從一般廣義子句集S出發到α的α廣義歸結演繹ω.證畢.

3 結束語

在基于格蘊涵代數的格值一階邏輯系統LF(X)中,筆者推廣了傳統的α歸結原理,將廣義子句集上的歸結問題推廣到一般廣義子句集上,即歸結過程中的子句將直接使用一般廣義子句,而不再轉換為合取范式,使歸結過程更加直觀、自然.筆者基于格值一階邏輯系統提出了一般廣義子句集上的α廣義歸結原理,建立了該原理的可靠性定理,通過提升引理給出了α廣義歸結原理的弱完備性定理.這些研究工作將為進一步探索基于格值邏輯系統的α廣義歸結方法奠定一定的基礎.

[1]Robinson J P.A Machine-Oriented Logic Based on the Resolution Principle[J].Journal of ACM,1965,12(1):23-41.

[2]Chang C L,Lee R C T.Symbolic Logic and Mechanical Theorem Proving[M].New York:Academic Press,1973.

[3]Wos L.Automated Reasoning:33 Basic Research Problems[M].Englewood Cliffs:Prentice Hall,1988.

[4]Xu Y,Ruan D,Qin K Y,et al.Lattice-Valued Logic—an Alternative Approach to Treat Fuzziness and Incomparability [M].New York:Springer-Verlag,2003.

[5]Sofronie-Stokkermans V.Automated Theorem Proving by Resolution in Non-Classical Logics[J].Annals of Mathematics and Artificial Intelligence,2007,49(1-4):221-252.

[6]Riva A,Nuzzo A,Stefanelli M,et al.An Automated Reasoning Framework for Translational Research[J].Journal of Biomedical Informatics,2010,43(3):419-427.

[7]Lu Zhirui,Augusto J,Liu Jun,et al.A Linguistic Truth-Value Temporal Reasoning(LTR)System and Its Application to the Design of an Intelligent Environment[J].International Journal of Computational Intelligence Systems,2012,5(1):173-196.

[8]王湘浩,劉敘華.廣義歸結[J].計算機學報,1982,5(2):81-92. Wang Xianghao,Liu Xuhua.Generalized resolution[J].Chinese Journal of Computers,1982,5(2):81-92.

[9] 劉敘華.基于歸結方法的自動推理[M].北京:科學出版社,1994.

[10]徐揚.格蘊涵代數[J].西南交通大學學報,1993,89(1):20-27. Xu Yang.Lattice Implication Algebra[J].Journal of Southwest Jiaotong University,1993,89(1):20-27.

[11]Xu Y,Liu J,Song Z M,et al.On Semantics of L-Valued First-Order Logic Lvft[J].International Journal General Systems,2000,29(1):53-79.

[12]Xu Y,Ruan D,Kerre E E,et al.α-Resolution Principle based on First-Order Lattice-Valued Logic LF(X)[J]. Information Sciences,2001,132(1-4):221-239.

[13]Xu Y,Ruan D,Kerre E E,et al.α-Resolution Principle based on Lattice-Valued Propositional Logic LP(X)[J]. Information Sciences,2000,130(1-4):195-223.

[14]Xu Y,Liu J,Ruan D,et al.Determination ofα-resolution in Lattice-valued First-order Logic LF(X)[J].Information Sciences,2011,181(10):1836-1862.

[15]徐揚.基于格值邏輯的語言真值α-廣義歸結自動推理研究[J].學術動態(西南交通大學),2009,(4):1-12. Xu Yang.Linguistic Truth-valuedα-generalized Resolution Automated Reasoning Research Based on Lattice-valued Logic [J].Xushu Dongtai(Southwest Jiaotong University),2009,(4):1-12.

[16]Xu Y,Xu W T,Zhong X M,et al.α-Generalized Resolution Principle Based on Lattice-valued Propositional Logic LP(X)[C]//Proceedings of the 9th International FLINS Conference.Singapore:World Scientific Publishing,2010:66-71.

(編輯:李恩科)

α-generalized resolution principle based on the lattice-valued first-order logic system

XU Weitao1,ZH ANG Wenqiang1,XU Yang2,ZH ANG Dexian1
(1.College of Information Science and Engineering,Henan Univ.of Technology,Zhengzhou 450001,China;2.School of Mathematics,Southwest Jiaotong Univ.,Chengdu 610031,China)

In the framework of the lattice-valued logic system based on the lattice implication algebra,the α-resolution principle based on the lattice-valued logic system is extended from generalized clauses set to general generalized clauses set.In this paper,theα-generalized resolution principle is presented in the lattice-valued first-order logic system LF(X).At the same time,the soundness theorem is established in LF(X).By using the lift lemma,the weak completeness theorem is also proved.This work can provide a new automated reasoning technology in order to establish novel generalized resolution methods for latticevalued logic systems.

lattice-valued first-order logic;general generalized clause;local extremely complex generalized literal;generalized resolution;automated reasoning

TP391

A

1001-2400(2014)01-0135-05

10.3969/j.issn.1001-2400.2014.01.024

2012-11-08 < class="emphasis_bold">網絡出版時間:

時間:2013-09-16

國家自然科學基金資助項目(61175055);國家自然科學青年基金資助項目(61300123);國家高技術研究發展計劃(863計劃)資助項目(2012AA101608);河南省教育廳自然科學資助項目(13B520945);河南工業大學高層次人才基金資助項目(2012BS012)

許偉濤(1979-),男,講師,博士,E-mail:hnxmxwt@163.com.

http://www.cnki.net/kcms/detail/61.1076.TN.20130916.0926.201401.168_020.html