模糊命題模態(tài)邏輯的Tableau方法

劉磊,王強(qiáng),呂帥,2

(1.吉林大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，吉林 長春 130012； 2.吉林大學(xué) 數(shù)學(xué)學(xué)院, 吉林 長春 130012)

?

模糊命題模態(tài)邏輯的Tableau方法

劉磊1,王強(qiáng)1,呂帥1,2

(1.吉林大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，吉林 長春 130012； 2.吉林大學(xué) 數(shù)學(xué)學(xué)院, 吉林 長春 130012)

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

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

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

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

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

1 模糊關(guān)系

對于一個模糊斷言,它的模糊度量值表示該P(yáng)ML公式成立的程度,是對PML公式進(jìn)行模糊化處理的結(jié)果。對模糊Kripke模型中的等價關(guān)系R進(jìn)行模糊化處理得到模糊關(guān)系,用以描述當(dāng)前可能世界ω和其相鄰可及世界υ的等價關(guān)系成立的程度。

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

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

證明:

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

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

證畢。

定理1 若一條可能世界的路徑序列為ω1,ω2,… ,ωn,且相鄰的兩個可能世界均存在等價關(guā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 假設(shè)圖1中的條件成立,ω是當(dāng)前可能世界,υ1、υ2、υ3是ω的三個相鄰可及世界,τ1、τ2是υ1的兩個相鄰可及世界,τ3、τ4、τ5是υ2的三個相鄰可及世界。它們之間的模糊關(guān)系表示如下

[(ω,υ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]

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

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

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

事實(shí)上,由于等價關(guān)系的性質(zhì),只要給定了相鄰的可能世界的模糊度量值,可以求得該路徑序列上任意2個可能世界的模糊關(guān)系的模糊度量值。模糊斷言集合事實(shí)上可以通過約簡策略來進(jìn)行約簡。模糊關(guān)系的定義與模糊斷言的定義相似,只是模糊關(guān)系的有序?qū)Φ那鞍氩糠钟脕砻枋隹赡苤g的等價關(guān)系,而模糊斷言的有序?qū)Φ那鞍氩糠钟脕砻枋雒}模態(tài)公式,因此模糊關(guān)系中也可以使用約簡策略,如例1中,因?yàn)樗枋鍪窃谀B(tài)S5系統(tǒng)下的FPML,因此R一定為等價關(guān)系,而由[(υ1,τ1):R,0.1]可以得到[(τ1,υ1):R,0.1],由[(ω,τ1):R,0.02]和[(τ1,υ1):R,0.1]可以得到[(ω,υ1):R,0.002]。需要強(qiáng)調(diào)的一點(diǎn)是:[(ω,υ1):R,0.002]與[(ω,υ1):R,0.2]并不矛盾,通過約簡規(guī)則可以由[(ω,υ1):R,0.2]將[(ω,υ1):R,0.002]刪除。在可能性邏輯中,若兩個命題公式成立的程度不一致時,可能性高的斷言可以約簡掉可能性低的斷言。在計(jì)算過程中,若出現(xiàn)從后繼世界來逆推模糊度量值時,會導(dǎo)致模糊度量值趨近于0,因此只考慮從前一個世界向其后繼世界的計(jì)算。

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

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

2 擴(kuò)展Tableau規(guī)則

本節(jié)結(jié)合傳統(tǒng)的模態(tài)邏輯中使用的Tableau規(guī)則給出了在FPML中的基本推理規(guī)則以及在推理過程所使用到的約簡策略,利用Tableau規(guī)則可以對給定的模糊斷言集合中的模糊斷言進(jìn)行處理。

2.1 推理規(guī)則

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

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

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

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

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

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

()

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

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

定理3 ◇-規(guī)則是正確的。

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

證畢。

2.2 約簡策略

在FPML中使用Tableau方法時,終止條件為推導(dǎo)出沖突或不能再使用表規(guī)則進(jìn)行推演。下面給出FPML中的沖突定義。

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

<φ,α>,<φ,β>

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

根據(jù)文獻(xiàn)[16]可以得到如下定義:

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

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

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

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

通過FPML的不一致性定義,可以在對FPML使用Tableau方法推理時,計(jì)算產(chǎn)生沖突的不一致估值,因?yàn)槭褂肨ableau方法進(jìn)行推理時,一定是通過使用表規(guī)則推導(dǎo)出沖突或者不能再使用表規(guī)則而終止,因此當(dāng)推導(dǎo)出沖突的時候,一定可以計(jì)算出Σ的不一致估值,由此可以對所要處理的模糊斷言集合進(jìn)行一致性檢測。

模態(tài)邏輯使用Tableau方法進(jìn)行推理時,因?yàn)樗獦?gòu)造的Tableau有限樹過于復(fù)雜,經(jīng)常會增加一些剪枝策略來加快求解,快速判斷有限樹的某個分支是否含有沖突,從而得到模態(tài)公式的可滿足性。FPML是PML的推廣,它在PML的基礎(chǔ)上增加了模糊度量值表示某個PML公式在可能世界中有效的程度,模糊度量值的加入使得模糊斷言集合的規(guī)模急劇增長,因?yàn)樵谀：龜嘌约现?同一個公式可能會有不同的度量值,也就是說存在兩個模糊斷言,它們的PML公式部分相同,而模糊度量值部分不同。在推理過程中,可以使用一些相應(yīng)的約簡策略來對模糊斷言集合進(jìn)行約簡,從而減少模糊斷言集合的規(guī)模。

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

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

1)若PML公式為φ,當(dāng)φ不含模態(tài)算子時,φ是命題公式,上述性質(zhì)顯然成立。

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

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

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

證畢。

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

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

此推論又可看作是MP規(guī)則在FPML中的推廣,也類似于可能性邏輯中提到的歸結(jié)方法[16],因?yàn)棣铡着cφ∨ψ是等價的,其證明過程與歸結(jié)方法的證明過程類似,在此不贅述。

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

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

文中提到針對模態(tài)邏輯的理論研究一般是在模態(tài)系統(tǒng)中進(jìn)行的,不同的模態(tài)系統(tǒng)的性質(zhì)又各不相同[16],在S5公理系統(tǒng)中,可以使用S5規(guī)約定理。

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

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

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

Procedure TFPML(Tableau in fuzzy proposition modal logic)

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

2)IfΣ=? Then return consistent

3)While ∑不含有沖突 do

While 可以用規(guī)則集RED依次化簡Σdo 用RED化簡Σ

EndWhile

If 不 能用表規(guī)則集合RT對Σ進(jìn)行推演

Then return consistent

Else 用表規(guī)則集合RT對Σ進(jìn)行推演

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

Σ=Σ-Σ1

將新推導(dǎo)出的模糊斷言放入集合Σ2

Σ=Σ∪Σ2

EndIf

EndWhile

4) return inconsistent

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

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

證畢。

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

Procedure CID(computing the Inconsistent degree)

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

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

用RED化簡Σ

EndWhile

3)While 可以用表規(guī)則集合RT對Σ進(jìn)行推演 do

用表規(guī)則集合RT對Σ進(jìn)行推演

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

Σ=Σ-Σ1

將新推導(dǎo)出的模糊斷言放入集合Σ2

Σ=Σ∪v2

While 可以用規(guī)則集RED依次化簡Σdo

用RED化簡Σ

Endwhile

EndWhile

4)IfΣ含有沖突

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

Else return 0

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

4 實(shí)例分析

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

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

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

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

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

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

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

下面考慮一個更為復(fù)雜的例子。

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

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

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

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

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

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

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

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

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

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

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

5 結(jié)論

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

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

[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]劉全,崔志明,高陽,等.一種邏輯強(qiáng)化學(xué)習(xí)的tableau推理方法[J].智能系統(tǒng)學(xué)報(bào),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]郝國舜,馬世龍,眭躍飛.一種擴(kuò)展的動態(tài)描述邏輯語言及其Tableau算法[J].智能系統(tǒng)學(xué)報(bào),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]郭新峰,馬世龍,呂江花,等.擴(kuò)展斷言知識檢驗(yàn)一致的需求建模方法[J].智能系統(tǒng)學(xué)報(bào),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推理規(guī)則簡化方法[J].計(jì)算機(jī)學(xué)報(bào),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算法的優(yōu)化及模型規(guī)約技術(shù)[J].計(jì)算機(jī)學(xué)報(bào), 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]周北海. 模態(tài)邏輯導(dǎo)論[M]. 北京：北京大學(xué)出版社, 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.

本文引用格式：

劉磊,王強(qiáng), 呂帥. 模糊命題模態(tài)邏輯的Tableau方法[J]. 哈爾濱工程大學(xué)學(xué)報(bào)， 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. 網(wǎng)絡(luò)出版日期：2017-03-30.

國家自然科學(xué)基金項(xiàng)目(61300049，61402195)；教育部高等學(xué)校博士學(xué)科點(diǎn)專項(xiàng)科研基金項(xiàng)目(20120061120059)；吉林省科技發(fā)展計(jì)劃項(xiàng)目(20130206052GX，20140520069JH).

劉磊(1960-), 男, 教授, 博士生導(dǎo)師； 呂帥(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