模糊命題模態邏輯的Tableau方法

劉磊,王強,呂帥,2

(1.吉林大學 計算機科學與技術學院，吉林 長春 130012； 2.吉林大學 數學學院, 吉林 長春 130012)

?

模糊命題模態邏輯的Tableau方法

劉磊1,王強1,呂帥1,2

(1.吉林大學 計算機科學與技術學院，吉林 長春 130012； 2.吉林大學 數學學院, 吉林 長春 130012)

為提高模糊命題模態邏輯(fuzzy propositional modal logic, FPML)的推理能力,本文將經典模態邏輯中的Tableau方法推廣到FPML中,提出了基于FPML的Tableau規則并證明了其正確性,給出了模糊斷言集合的約簡策略;在此基礎上給出了FPML中的不一致性和不一致估值的定義。最后給出基于Tableau方法的FPML的一致性檢測方法TFPML和模糊斷言集合的不一致估值計算方法CID,并證明了其正確性。實例分析表明,本文提出的方法是正確有效的。

Tableau方法；模態邏輯；模糊命題模態邏輯；不確定推理；一致性檢測；模糊斷言集合

自動推理隸屬人工智能領域,也是理論計算機科學的一個重要組成部分,主要用來進行自動定理證明,通常用來判定某個公式的有效性或可滿足性,在模態邏輯、描述邏輯、時態邏輯等非經典邏輯中也有廣泛應用[1-3]。模態邏輯自提出以來,研究人員針對不同的模態系統提出了很多有效的推理方法,包括模態Tableau方法、模態歸結方法[4]、基于關系轉換的方法[5-6]等。可能性邏輯是經典命題邏輯的擴充,是用于解決不確定知識表示和推理的邏輯,類比地在模態邏輯中,為了解決含有不確定知識的表示與推理。Hájek提出了模糊模態邏輯(fuzzy modal logic， FML),并提出了一種在模糊S5系統中的公理化方法,將模態邏輯中的等價關系對應到了FML中的不一致關系[7-8]。

命題模態邏輯(propositional modal logic， PML)是模態邏輯的一種最經典形式,模糊命題模態邏輯(fuzzy propositional modal logic， FPML)是PML的推廣。FPML是在PML的基礎上加入了隸屬度因子n,對于后者而言，n∈{0,1}；對于前者，n∈[0,1]。目前,基于FPML的推理方法大多使用演繹方法。Tableau方法是一種完備的推理方法[9-11],且在經典邏輯與非經典邏輯的知識表示與推理過程中應用廣泛。在國內,劉全等提出了一種基于布爾剪枝的多值廣義量詞Tableau推理規則簡化方法,對含廣義量詞(交和并)規則的簡化方法進行研究,建立了一套含廣義量詞的一階多值邏輯公式的簡化Tableau推理方法,該方法將傳統的Tableau方法基礎上,簡化了一階多值邏輯公式中的規則,提高了推理效率[12]。劉大有等結合沖突技術和矛盾學習技術實現了針對模態系統S4的推理機S4P,且效率優于著名的描述邏輯求解器RACER和FACT++[13],S4P中包含兩種Tableau算法優化技術，即沖突技術和矛盾學習技術,沖突技術利用否定范式的沖突來確定公式集的不一致性,而矛盾學習技術利用增加的矛盾原因集來減少節點的擴展,這是Tableau方法在經典模態系統S4中的成功運用。在國外也有很多基于Tableau方法的改進和推廣,Tao等提出一種PSPACE Tableau算法,對描述邏輯進行了擴展,在其中增加了多模態邏輯K(m)和S4(m)中的模態算子[14],極大地提高了描述邏輯的表達能力。Hidalgo-Doblado等提出了一種基于描述邏輯的形式校驗的Tableau算法[15],詳細說明了基于Tableau算法的規則應用與分支選擇策略,提高了描述邏輯ALC的推理效率。因此將Tableau方法加以推廣應用在FPML推理中有益于Tableau方法的更進一步深入研究與應用。

非經典邏輯的描述和表示較為復雜,多用Tableau方法來進行求解或證明,如經典模態邏輯和經典描述邏輯中Tableau方法的使用尤為廣泛。但是有關FPML的Tableau方法及其對應的推理規則在國內外未見報到,因此本文將經典模態邏輯中的Tableau方法推廣到FPML中,可以用來對不同模態邏輯的不確定知識進行表示和預測,以及不確定性知識庫的一致性判定等。本文提出基于FPML的Tableau規則,給出模糊斷言集合的約簡策略;在此基礎上給出FPML中的不一致性和不一致估值的定義;最后給出基于Tableau方法的FPML一致性檢測方法和模糊斷言集合的不一致估值計算方法,并證明其正確性。

1 模糊關系

對于一個模糊斷言,它的模糊度量值表示該PML公式成立的程度,是對PML公式進行模糊化處理的結果。對模糊Kripke模型中的等價關系R進行模糊化處理得到模糊關系,用以描述當前可能世界ω和其相鄰可及世界υ的等價關系成立的程度。

定義1 FPML中的模糊關系表示為一個有序對[(ω,υ):R,η],其中(ω,υ):R表示可能世界ω和可能世界υ具有等價關系,η為模糊關系的模糊度量值,表示可能世界ω及可能世界υ具有等價關系的程度。

引理1 設ω是當前可能世界,υ是ω的相鄰可及世界,τ是υ的相鄰可及世界,且滿足ω和υ的模糊關系為[(ω,υ):R,η1],υ和τ的模糊關系為[(υ,τ):R,η2],則有:[(ω,υ):R,η1],[(υ,τ):R,η2] iff [(ω,τ):R,η3]且η3=η1×η2。

證明:

充分性。根據已知條件,可知ω、υ、τ在同一條可達世界路徑上,因為[(ω,τ):R,η3]成立且R為等價關系(自反,傳遞,對稱),所以對于可達路徑上的ω和υ、υ和τ也有等價關系;由于ω和τ的模糊關系大小η3是由ω和υ的模糊關系與υ和τ的模糊關系共同決定的,所以η3=η1×η2。

必要性。已知有[(ω,υ):R,η1],[(υ,τ):R,η2]成立,且R為等價關系(自反、傳遞、對稱),因此ω和τ也存在R關系,容易知道ω,υ,τ在同一條可達世界路徑上,ω和υ具有等價關系的程度、υ和τ具有等價關系的程度二者共同決定了ω和τ具有等價關系的程度,因此有[(ω,τ):R,η3]成立,且η3=η1×η2。

證畢。

定理1 若一條可能世界的路徑序列為ω1,ω2,… ,ωn,且相鄰的兩個可能世界均存在等價關系,則:

[(ω1,ω2):R,η1],[(ω2,ω3):R,η2],…,[(ωn-1,ωn):R,ηn-1] iff [(ωi,ωj):R,ηi×…×ηj-1](i

由引理1容易得證,在此不贅述。

例1 假設圖1中的條件成立,ω是當前可能世界,υ1、υ2、υ3是ω的三個相鄰可及世界,τ1、τ2是υ1的兩個相鄰可及世界,τ3、τ4、τ5是υ2的三個相鄰可及世界。它們之間的模糊關系表示如下

[(ω,υ1):R,0.2],[(ω,υ2):R,0.4],[(ω,υ3):R,0.6],[(υ1,τ1):R,0.1],[(υ1,τ2):R,0.3],[(υ2,τ3):R,0.5],[(υ2,τ4):R,0.7],[(υ2,τ5):R, 0.9]

根據定理1可知,圖1中所有的可達路徑序列為(ω,υ1,τ1),(ω,υ1,τ2),(ω,υ2,τ3),(ω,υ3,τ4),(ω,υ2,τ5),(ω,υ3),除已知的模糊關系外,可以計算出如下可達世界的模糊關系:

[(ω,τ1):R,0.02],[(ω,τ2):R,0.06],[(ω,τ3):R,0.2],[(ω,τ4):R,0.28],[(ω,τ5):R,0.36]

圖1 可能世界及其模糊關系Fig.1 The possible worlds and their fuzzy relations

事實上,由于等價關系的性質,只要給定了相鄰的可能世界的模糊度量值,可以求得該路徑序列上任意2個可能世界的模糊關系的模糊度量值。模糊斷言集合事實上可以通過約簡策略來進行約簡。模糊關系的定義與模糊斷言的定義相似,只是模糊關系的有序對的前半部分用來描述可能之間的等價關系,而模糊斷言的有序對的前半部分用來描述命題模態公式,因此模糊關系中也可以使用約簡策略,如例1中,因為所描述是在模態S5系統下的FPML,因此R一定為等價關系,而由[(υ1,τ1):R,0.1]可以得到[(τ1,υ1):R,0.1],由[(ω,τ1):R,0.02]和[(τ1,υ1):R,0.1]可以得到[(ω,υ1):R,0.002]。需要強調的一點是:[(ω,υ1):R,0.002]與[(ω,υ1):R,0.2]并不矛盾,通過約簡規則可以由[(ω,υ1):R,0.2]將[(ω,υ1):R,0.002]刪除。在可能性邏輯中,若兩個命題公式成立的程度不一致時,可能性高的斷言可以約簡掉可能性低的斷言。在計算過程中,若出現從后繼世界來逆推模糊度量值時,會導致模糊度量值趨近于0,因此只考慮從前一個世界向其后繼世界的計算。

定理2 在一個模糊關系集合中,若存在模糊關系[(ω,υ):R,α]與[(ω,υ):R,β],α和β是關于ω和υ的模糊關系的模糊度量值,且α≠β,則可以將模糊度量值較小的模糊斷言刪除,即用<φ,max(α,β)>替換<φ,α>和<φ,β>。

證明: 在可能性邏輯中,當α≥β時,有(φ,α)├(φ,β)[16]。在此,可以將ω和υ具有等價關系當作一個命題p,且該命題是二值的,當α≥β時,等同于可能性邏輯中,可得(p,α)├(p,β),定理得證。

2 擴展Tableau規則

本節結合傳統的模態邏輯中使用的Tableau規則給出了在FPML中的基本推理規則以及在推理過程所使用到的約簡策略,利用Tableau規則可以對給定的模糊斷言集合中的模糊斷言進行處理。

2.1 推理規則

∧-規則:即模態邏輯中的α規則的推廣,公式φ∧ψ成立的程度決定公式φ和公式ψ分別成立的程度,形式地:

∨-規則:即模態邏輯中的β規則的推廣,若公式φ∨ψ成立的程度為α,則公式φ成立的程度為α或公式ψ成立的程度為α,形式地:

□-規則:對于含必然算子的命題模態公式而言,它的模糊斷言和所在世界與后繼可能世界的模糊關系共同決定它在后繼可能世界的模糊斷言的形式,且后繼可能世界中的模糊度量值為當前世界的模糊度量值與模糊關系的最小值,形式地:

◇-規則:對于含有可能算子的模態公式而言,若在后繼可能世界中,不存在模糊斷言和模糊關系使得它們的模糊度量值都大于當前世界的可能性估值,則可以用當前世界的模糊度量值代替它們的模糊度量值,形式地:

ζ表示存在一個υ使得有<υ:φ,β>,[(ω,υ):R,γ],且min(β,γ)≥α。

在使用◇-規則時,必須保證在可能世界υ中,模糊斷言<υ:φ,β>和模糊關系[(ω,υ):R,γ]的可能性度量至少有一個比α小,這樣在可能世界υ中推導出來的模糊斷言α大于β或者γ。

()

⊥-規則:若兩個模糊斷言有沖突,可以用一個模糊斷言來替換,其公式部分為⊥,模糊度量值為約簡前的兩個模糊斷言的模糊度量值的最小值,形式地:

相比較于其他規則,◇-規則比較難以理解,在此給出證明過程。

定理3 ◇-規則是正確的。

證明: 使用反證法來進行證明,假設ζ成立,那么在可能世界υ中,有模糊斷言<υ:φ,β>和模糊關系[(ω,υ):R,γ],且min(β,γ)≥α,根據引理2,可以用<υ:φ,β>替換掉<υ:φ,α>,即所推導出的<υ:φ,α>是無效的。所以假設不成立,◇-規則是正確的。

證畢。

2.2 約簡策略

在FPML中使用Tableau方法時,終止條件為推導出沖突或不能再使用表規則進行推演。下面給出FPML中的沖突定義。

定義2Σ是模糊斷言集合,φ為任意的PML公式,若∑中同時包含如下兩個模糊斷言:

<φ,α>,<φ,β>

稱Σ包含一個沖突⊥,若Σ中存在沖突,那么Σ是不一致的,利用沖突規則可以將兩個沖突的模糊斷言約簡為一個模糊斷言,即<⊥,min(α,β)>。

根據文獻[16]可以得到如下定義:

定義3Σ是模糊斷言集合,Σ的不一致性估值為

Inc(Σ)=max{α|Σ╞<⊥,α>}

定義4 設Σ1=<φ∨ψ,α>∪Σ,Σ2=<φ,α>∪Σ,Σ3=<ψ,α>∪Σ,則有

Inc(Σ1)=min(Inc(Σ2),Inc(Σ3))

通過FPML的不一致性定義,可以在對FPML使用Tableau方法推理時,計算產生沖突的不一致估值,因為使用Tableau方法進行推理時,一定是通過使用表規則推導出沖突或者不能再使用表規則而終止,因此當推導出沖突的時候,一定可以計算出Σ的不一致估值,由此可以對所要處理的模糊斷言集合進行一致性檢測。

模態邏輯使用Tableau方法進行推理時,因為所要構造的Tableau有限樹過于復雜,經常會增加一些剪枝策略來加快求解,快速判斷有限樹的某個分支是否含有沖突,從而得到模態公式的可滿足性。FPML是PML的推廣,它在PML的基礎上增加了模糊度量值表示某個PML公式在可能世界中有效的程度,模糊度量值的加入使得模糊斷言集合的規模急劇增長,因為在模糊斷言集合中,同一個公式可能會有不同的度量值,也就是說存在兩個模糊斷言,它們的PML公式部分相同,而模糊度量值部分不同。在推理過程中,可以使用一些相應的約簡策略來對模糊斷言集合進行約簡,從而減少模糊斷言集合的規模。

引理2 若在模糊斷言集合中同時存在模糊斷言<φ,α>和<φ,β>,φ是任意的模態公式,α和β是公式φ的模糊度量值,且α≠β,則可以將模糊度量值較小的模糊斷言刪除,即用<φ,max(α,β)>替換<φ,α>和<φ,β>。

證明: 在可能性邏輯中,當α≥β時,有(φ,α)├(φ,β)[16]。FPML中將可能性邏輯中的命題公式換成了PML公式,下面證明對于PML公式來說,也有這樣的性質存在:

1)若PML公式為φ,當φ不含模態算子時,φ是命題公式,上述性質顯然成立。

2)若PML公式為□φ,根據T公理可知,在當前世界ω上述性質成立;φ在后繼可能世界υ中模糊度量值是由φ在當前世界ω的度量值以及ω與υ的模糊關系共同決定的,而針對于<□φ,α>和<□φ,β>而言,當前世界ω與后繼可能世界υ的模糊關系一定是相同的,因此α和β的偏序關系在所有的后繼世界中都不會改變,因此對于模態公式□φ來說,上述性質是成立的。

3)若PML公式為◇φ,其在模態邏輯下的定義是存在某個與當前世界相鄰的后繼可能世界使得φ成立,因此只考慮在可能世界υ中的情況,根據◇-規則,當滿足其使用條件時,有如下替換成立:

對于<◇φ,α>和<◇φ,β>,在可能世界υ中,α和β的偏序關系也不會發生改變,因此上述性質成立。

證畢。

例2 已知Σ={<ω:□φ,0.8>,<ω:□φ,0.6>},在當前世界ω中,<φ,0.8>,<φ,0.6>一定成立,可以進行約簡,滿足性質;當ω與υ的模糊關系為[(ω,υ):R,0.3]時,在可能世界υ中有<υ:φ,0.3>,兩者在可能世界υ中的映射是相同的;而當ω與υ的模糊關系為[(ω,υ):R,0.9]時,則在可能世界υ中有<υ:φ,0.8>,<υ:φ,0.6>,兩者在可能世界υ中的映射偏序關系保持不變;而當ω與υ的模糊關系為[(ω,υ):R,0.7]時,則在可能世界υ中有<υ:φ,0.7>,<υ:φ,0.6>,兩者在可能世界υ中的映射偏序關系仍保持不變,所以通過引理2可以將∑約簡成∑′={<ω:□φ,0.8>}。

推論1 若在∑中同時存在模糊斷言<φ→ψ,α>和<φ,β>,可以用<ψ,min(α,β)>替換<φ→ψ,α>。

此推論又可看作是MP規則在FPML中的推廣,也類似于可能性邏輯中提到的歸結方法[16],因為φ→ψ與φ∨ψ是等價的,其證明過程與歸結方法的證明過程類似,在此不贅述。

應用以上引理和推論可以對要處理的模糊斷言集合進行預處理,刪除掉一些不必要的模糊斷言,從而降低模糊斷言集合的規模,對剩余模糊斷言使用Tableau方法求解,盡快找到沖突,計算模糊斷言集合的不一致性。

3 模糊斷言集合的一致性檢測

文中提到針對模態邏輯的理論研究一般是在模態系統中進行的,不同的模態系統的性質又各不相同[16],在S5公理系統中,可以使用S5規約定理。

定理4[17](S5規約定理)在S5系統中,對于任意的模態公式,若其模態詞的嵌套層數大于1,則可以對其進行規約,使得公式的模態詞的個數不大于1,從而大大降低了公式復雜度和規模。

本文的所有推理過程都是在模糊S5系統中進行的,對模糊斷言集合中的任一模糊斷言,都可以使用規約定理對其PML公式部分進行歸約,使公式的模態度小于或等于1。設模糊斷言集合為Σ={Δ1,Δ2，… ,Δn},Δn表示n個模糊斷言。約簡策略的集合為RED={R1,R2},R1和R2分別為

表規則集合為RT={R∧,R∨,R□,R◇,R,R⊥}。下面給出關于模糊斷言集合∑一致性檢測的過程的形式化描述:

Procedure TFPML(Tableau in fuzzy proposition modal logic)

1)輸入:模糊斷言集合Σ={Δ1,… ,Δn}

2)IfΣ=? Then return consistent

3)While ∑不含有沖突 do

While 可以用規則集RED依次化簡Σdo 用RED化簡Σ

EndWhile

If 不 能用表規則集合RT對Σ進行推演

Then return consistent

Else 用表規則集合RT對Σ進行推演

將被約簡的模糊斷言放入集合Σ1

Σ=Σ-Σ1

將新推導出的模糊斷言放入集合Σ2

Σ=Σ∪Σ2

EndIf

EndWhile

4) return inconsistent

定理5 過程TFPML是正確完備的。

證明:若Σ=?,Σ是一致的,在第二行返回consistent,否則判斷Σ是否含有沖突。若Σ含有沖突,則Σ是不一致的,退出循環,返回inconsistent,否則使用規則集RED對Σ進行化簡,引理2和推論1保證了RED化簡的正確性。若對Σ使用表規則的過程中產生了沖突,那么Σ一定是不一致的,退出循環,返回inconsistent,否則對Σ循環使用表規則集RT,直到不能使用RT為止,若此時仍沒有產生沖突,那么Σ是一致的,返回consistent。Tableau方法在使用Tableau規則時,每一步都可以給出對應的樹結構,在推理樹中,葉節點都是原子的,即在此處不能再使用Tableau規則。因此算法一定會終止。

證畢。

對于任意給定的模糊斷言集合Σ,都可以使用TFPML方法對Σ進行一致性檢測,若Σ是不一致的,往往需要給出不一致性估值來表示其不一致程度。下面給出一致性檢測的一致性估值的計算方法過程的形式化描述:

Procedure CID(computing the Inconsistent degree)

1)輸入:模糊斷言集合Σ={Δ1,Δ… ,Δn}

2)While 可以用規則集RED依次化簡Σdo

用RED化簡Σ

EndWhile

3)While 可以用表規則集合RT對Σ進行推演 do

用表規則集合RT對Σ進行推演

將被約簡的模糊斷言放入集合Σ1

Σ=Σ-Σ1

將新推導出的模糊斷言放入集合Σ2

Σ=Σ∪v2

While 可以用規則集RED依次化簡Σdo

用RED化簡Σ

Endwhile

EndWhile

4)IfΣ含有沖突

Then return 沖突模糊斷言的模糊度量值

Else return 0

CID與TFPML的思想基本相同,TFPML只要歸約出沖突,立即退出循環,并返回inconsistent;而CID為了要計算不一致估值,需要對Σ不斷地使用表規則集RT,直到不能使用表規則集RT為止,并在使用表規則集RT的同時使用規則集RED對Σ進行歸約,若包含多個沖突模糊斷言,則歸約過后只會留下模糊度量值最大的沖突斷言。最后進行判斷,若有沖突,則返回沖突模糊斷言的模糊度量值,即不一致估值,否則返回0。因此,計算不一致估值的方法CID也是正確完備的。

4 實例分析

本文將可能性邏輯中的不一致定義和不一致估值計算方法擴展到了FPML中,給出了模糊斷言集合的不一致性定義及其不一致估值的計算方法,提出了基于Tableau方法的FPML一致性檢測方法TFPML和不一致估值計算方法CID,并在兩種方法的過程中加入了約簡策略,驗證了約簡策略和所提出方法的正確完備性,約簡策略有利于及時地對模糊斷言集合進行約簡,能夠提高推理效率。

FPML是PML的并不像模態邏輯和命題邏輯那樣有標準的Benchmark問題[18],尚未出現關于FPML的模糊斷言測試集,因此本文基于模糊描述邏輯中的實例[19],構造了FPML的實例,通過實例來演示推理過程,同時也進一步驗證了該計算方法的正確性。由于CID與TFPML的思想基本相同,TFPML只要歸約出沖突,立即退出循環,并返回inconsistent;而CID為了要計算不一致估值需要返回的是確定的模糊度量值,因此本文僅給出CID方法的過程。首先給出一個簡單的例子。

例3Σ={<φ,0.3>,<φ,0.1>,<ψ,0.5>,<φ→ψ,0.2>},計算該模糊斷言集合的不一致估值。

1)使用RED規則集的R1對Σ進行約簡,根據引理2,可以刪除<φ,0.1>,約簡后的模糊斷言集合Σ={<φ,0.3>,<ψ,0.5>,<φ→ψ,0.2>}。

2)使用RED規則集的R2對Σ進行約簡,根據推論1,可以用<ψ,0.2>代替<φ→ψ,0.2>,約簡后的模糊斷言集合Σ={<φ,0.3>,<ψ,0.5>,<ψ,0.2>}。

3)新增加的<ψ,0.2>與<ψ,0.5>產生沖突,使用R⊥規則得到<⊥,0.2>,約簡后的模糊斷言集合Σ={<φ,0.3>,<⊥,0.2>}。

4)此時不可以再使用表規則集RT對模糊斷言集合Σ進行約簡,也不能使用RED規則集對Σ進行約簡,Σ中有沖突,所以Σ是不一致的,且Σ的不一致估值為0.2,即Inc(Σ)=0.2。

下面考慮一個更為復雜的例子。

例4 設Σ={<ω:φ,0.3>,<ω:φ,0.1>,<ω:ψ,0.5>,<ω:□φ,0.6>,<ω:φ→ψ,0.2>,<ω:□□φ,0.3>,<υ:□◇(φ∧χ),0.4>,<υ:◇(φ∧ψ),0.2>,<ω:◇◇(φ∧ψ),0.8>,<ω:◇(φ∧ψ),0.8>},υ為ω的相鄰可及世界,計算Σ的不一致估值。

1)使用RED規則集的R1對Σ進行約簡,由于本文所處理的模態公式都是默認在S5系統中的,因此<ω:□□φ,0.3>與<ω:□φ,0.3>等價、<υ:□◇(φ∧χ),0.4>與<υ:◇(φ∧χ),0.4>等價、<ω:◇◇(φ∧ψ),0.8>與<ω:◇(φ∧ψ),0.8>等價,因此根據引理2,可以刪除<ω:φ,0.1>,<ω:□□φ,0.3>,<υ:◇(φ∧ψ),0.2>,<ω:◇◇(φ∧ψ),0.8>,約簡后的模糊斷言集合為:Σ={<ω:φ,0.3>,<ω:ψ,0.5>,<ω:□φ,0.6>,<ω:φ→ψ,0.2>,<υ:◇(φ∧ψ),0.4>,<ω:◇(φ∧ψ),0.8>}。

2)使用RED規則集的R2對Σ進行約簡,根據推論1,可以用<ψ,0.2>代替<φ→ψ,0.2>,約簡后的模糊斷言集合為Σ={<ω:φ,0.3>,<ω:ψ,0.5>,<ω:□φ,0.6>,<ω:ψ,0.2>,<υ:◇(φ∧χ),0.4>,<ω:◇(φ∧ψ),0.8>}。

3)新增加的<ω:ψ,0.2>與<ω:ψ,0.5>產生了沖突,使用R⊥規則得到<ω:⊥,0.2>,約簡后的模糊斷言集合為Σ={<ω:φ,0.3>,<ω:□φ,0.6>,<ω:⊥,0.2>,<υ:◇(φ∧χ),0.4>,<ω:◇(φ∧ψ),0.8>}。

4)對于模糊斷言<ω:◇(φ∧ψ),0.8>,由于在可能世界υ中,并不存在<υ:φ,β>,[(ω,υ):R,γ],且min(β,γ)≥0.8,因此ζ條件不成立,可以使用R◇規則,得到<υ:(φ∧ψ),0.8>,[(ω,υ):R,0.8]。假設υ的下一可能世界為τ,在可能世界τ中ζ條件也不成立,同理<υ:◇(φ∧χ),0.4>使用R◇規則得到<τ:(φ∧χ),0.4>,[(υ,τ):R,0.4],約簡后的模糊斷言集合為Σ={<ω:φ,0.3>,<ω:□φ,0.6>,<ω:⊥,0.2>,<τ:(φ∧χ),0.4>,<υ:(φ∧ψ),0.8>}。模糊關系集為

Г={[(ω,υ):R,0.8], [(υ,τ):R,0.4]}。

5)繼續使用表規則集合RT對模糊斷言集合Σ進行推演,<υ:(φ∧ψ),0.8>使用R∧規則得到<υ:φ,0.8>,<υ:ψ,0.8>,<τ:(φ∧χ),0.4>使用R∧規則得到<τ:φ,0.4>,<τ:χ,0.4>,此時模糊斷言集合為Σ={<ω:φ,0.3>,<ω:□φ,0.6>,<ω:⊥,0.2>,<τ:φ,0.4>,<τ:χ,0.4>,<υ:φ,0.8>,<υ:ψ,0.8>}。模糊關系集為Г={[(ω,υ):R, 0.8],[(υ,τ):R,0.4]}。

6)對于模糊斷言<ω:□φ,0.6>,使用R□規則得到<υ:φ,0.6>,而<υ:φ,0.6>與<υ:φ,0.8>使用R⊥規則得到<υ:⊥,0.6>,此時模糊斷言集合為:Σ={<ω:φ,0.3>,<ω:⊥,0.2>,<τ:φ,0.4>,<τ:χ,0.4>,<υ:⊥,0.6>,<υ:ψ,0.8>}。模糊關系集為

Г={[(ω,υ):R,0.8],[(υ,τ):R,0.4]}。

7)此時,對于模糊斷言集合Σ不可以再使用表規則集RT對模糊斷言集合Σ進行約簡,也不能使用RED規則集對Σ進行約簡,Σ中有沖突,所以Σ是不一致的,且Σ的不一致估值為所有沖突斷言中最大的模糊度量值,即Inc(Σ)=0.6。

例3、4表明,對任意給定的有限的模糊斷言集合,都可以通過擴展Tableau規則對其進行推演,且可以判斷模糊斷言集合的一致性。若給定的模糊斷言集合是不一致的,還可以通過CID方法計算出模糊斷言集合的不一致估值,即該集合的一致性程度,它描述了該集合有效的程度。

5 結論

1)擴展的Tableau規則可以應用于FPML,且在推理過程加入約簡策略可以較為高效地處理模糊斷言集中的不一致問題。

2)TFPML和CID是正確有效的,同時為Tableau方法在其他非經典邏輯或混合邏輯中的應用奠定了基礎。

[1]GOLISKA-PILAREK J, MUOZ-VELASCO E, MORA A. Deterministic tableau-decision procedure via reductions for modal logic K[J]. Advances in intelligent systems and computing, 2014, 239: 429-438.

[2]SCHMIDT R A, TISHKOVSKY D. Using tableau to decide description logics with full role negation and identity[J]. ACM transactions on computational logic, 2012, 15(1): 136-156.

[3]REYNOLDS M. A tableau for temporal logic over the reals[J]. Advances in modal logic, 2014, 10: 439-458.

[4]NALON C, DIXON C. Clasusal resolution for normal modal logics[J]. Journal of algorithms, 2007, 62: 117-134.

[5]ANGELO M, ALBERTO P, MATTEO S. Alternative translation techniques for propositional and first-order modal logics [J]. Journal of automated reasoning, 2002, 28(4): 397-415.

[6]MARK K, TOBIAS T. InKreSAT: Modal reasoning via incremental reduction to SAT[C]∥Proceedings of the 24th International Conference on Automated Deduction, Lake Placid, USA, 2013, 436-442.

[9]劉全,崔志明,高陽,等.一種邏輯強化學習的tableau推理方法[J].智能系統學報,2008,3(4):355-360.

LIU Quan, CUI Zhiming, GAO Yang, et al. Tableau reasoning method based on logical reinforcement learning [J]. CAAI transactions on intelligent systems, 2008, 3(4): 355-360.

[10]郝國舜,馬世龍,眭躍飛.一種擴展的動態描述邏輯語言及其Tableau算法[J].智能系統學報,2009,4(3):226-233.

HAO Guoshun, MA Shilong, SUI Yuefei. An extended dynamic description logic language and its Tableau algorithm[J]. CAAI transactions on intelligent systems, 2009, 4(3): 226-233.

[11]郭新峰,馬世龍,呂江花,等.擴展斷言知識檢驗一致的需求建模方法[J].智能系統學報,2015,10(1):81-90.

GUO Xinfeng, MA Shilong, LYU Jianghua, et al. Extension abox requirements modeling method[J]. CAAI transactions on intelligent systems, 2015, 10(1): 81-90.

[12]劉全,孫吉貴,崔志明.基于布爾剪枝的多值廣義量詞Tableau推理規則簡化方法[J].計算機學報,2005,28(9):1514-1518.

LIU Quan, SUN Jigui, CUI Zhiming. A method of simplifying many-valued generalized quantifiers Tableau rules based on boolean pruning[J]. Chinese journal of computers, 2005, 28(9): 1514-1518.

[13]劉大有,賴永,王生生.Tableau算法的優化及模型規約技術[J].計算機學報, 2014, 37(8): 1647-1657.

LIU Dayou, LAI Yong, WANG Shengsheng. Techniques about optimizing Tableau algorithm and reducing models[J]. Chinese journal of computers, 2014, 37(8): 1647-1657.

[14]TAO J, SLUTZKI G, HONAVAR, V. PSPACE Tableau algorithms for acyclic modalized ALC[J]. Journal of automated reasoning, 2012, 49(4): 551-582.

[15]HIDALGO-DOBLADO M J, ALONSO-JIMéNEZ J A, BORREGO-DAZ J, et al. Formally verified Tableau-based reasoners for a description logic[J]. Journal of automated reasoning, 2014, 52(3): 331-360.

[16]DUBOIS D, LANG J, PRADE H. Possibilistic logic [C]// In: GABBAY D, HOGGER C J, ROBINSON J A (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming. New York: Oxford University Press, 1994: 439-513.

[17]周北海. 模態邏輯導論[M]. 北京：北京大學出版社, 1997: 69-102.

ZHOU Beihai. Modal logic: an introduction[M]. Beijing: Peking University Press, 1997: 69-102.

[18]BALSIGER P, HEUERDING A, SCHWENDIMANN S. A benchmark method for the propositional modal logics K, KT, S4[J]. Journal of automated reasoning, 2000, 24(3): 297-317.

[19]STRACCIA U. Reasoning within fuzzy description logics[J]. Journal of artificial intelligence research, 2001, 14(1): 137-166.

本文引用格式：

劉磊,王強, 呂帥. 模糊命題模態邏輯的Tableau方法[J]. 哈爾濱工程大學學報， 2017， 38(6)： 914-920.

LIU Lei， WANG Qiang， LYU Shuai. Tableau approach of fuzzy propositional modal logic[J]. Journal of Harbin Engineering University， 2017， 38(6)： 914-920.

Tableau approach of fuzzy propositional modal logic

LIU Lei1， WANG Qiang1， LYU Shuai1,2

(1.College of Computer Science and Technology, Jilin University, Changchun 130012, China; 2.College of Mathematics, Jilin University, Changchun 130012, China)

In order to improve the reasoning ability of fuzzy propositional modal logic (FPML), we propose a tableau approach to FPML, including a reduction strategy and tableau rules based on FPML. We also propose a method known as tableau approach of fuzzy propositional modal logic (TFPML) to check the consistency of FPML, and a computing method known as CID to determine the degree of inconsistency of a fuzzy assertion set. The soundness and completeness of these two methods are proven, and their correctness and effectiveness are illustrated.

Tableau approach; modal logic; fuzzy propositional modal logic; uncertainty reasoning; consistency checking

2016-03-23. 網絡出版日期：2017-03-30.

國家自然科學基金項目(61300049，61402195)；教育部高等學校博士學科點專項科研基金項目(20120061120059)；吉林省科技發展計劃項目(20130206052GX，20140520069JH).

劉磊(1960-), 男, 教授, 博士生導師； 呂帥(1981-), 男, 副教授.

呂帥，E-mail：lus@jlu.edu.cn.

10.11990/jheu.201603080

http://www.cnki.net/kcms/detail/23.1390.u.20170330.0957.010.html

TP181

A

1006-7043(2017)06-0914-07