摘要:針對格值命題邏輯中歸結自動推理算法的效率問題,在格值命題邏輯系統中的α-歸結原理基礎上,提出了格值命題邏輯系統LP(X)上的II-α-超歸結原理,并證明了其可靠性和完備性。最后,通過一個具體的例子來說明II-α-超歸結原理對于提高自動推理算法的效率十分有效。
關鍵詞:格值命題邏輯系統;歸結自動推理;α-歸結原理;II-α-超歸結原理
中圖分類號:O153文獻標識碼:A文章編號:1009-3044(2009)33-9547-03
II-α-hyper Resolution Principle of Lattice-valued Propositional Logic LP(X)
LI Xiao-bing
(Department of Information Engineering, Dongbei University of Finance and Economics, Dalian 116025, China)
Abstract: In order to improve the efficiency of resolution automated reasoning algorithm in lattice-valued propositional logic, II-α-hyper resolution principle is proposed based onα- resolution principle of lattice-valued propositional logic LP(X). Its soundness and completeness are proved. Finally, the efficiency of II-α-hyper resolution principle is illustrated.
Key words: lattice-valued propositional logic; resolution automated reasoning; α- resolution principle; II-α-hyper resolution principle
人工智能是研究解釋和模擬人類智能行為及其規律的一門學科,其主要任務是建立智能信息處理理論和系統。在人工智能的眾多研究課題中,自動推理始終是一個重要的研究課題。這是因為推理與計算正是人類的智能活動的集中體現。人類對信息的處理離不開推理,有效的推理要求以一個可靠且完備的邏輯系統作為基礎。
格值邏輯作為一種重要的非經典邏輯,它能有效地刻畫人類的思維、判斷和決策的不確定性。為處理某些不確定性信息的推理問題,建立在格值邏輯系統[2-3]上的α-歸結理論[4]與方法[5-7]得到了快速發展。隨后很多文獻討論了格值命題邏輯系統LP(X)的α-歸結自動推理算法[7-9]。如何提高歸結自動推理算法的效率是實際應用中亟待解決且十分重要的問題。
1 預備知識
定義2.1[1] 設(L,∨,∧,′,→,O,I)是一個具有逆序對合“′”的且有泛界O和I的有界格,“→”是從L×L到L的映射,如果對任意的x, y, z∈L下列條件成立:
(I1) x→(y→z)= y→(x→z);
(I2) x→x= I;
(I3) x→y= y′→x′;
(I4) 如果x→y= y→x= I,則x= y;
(I5) (x→y)→y= (y→x)→x;
(I6) (x∨y)→z= (x→z) ∧(y→z);
(I7) (x∧y)→z= (x→z) ∨(y→z);
則稱(L,∨,∧,′,→,O,I)為格蘊涵代數。
定義2.2[2] 設X是命題變元集合,T=L∪{′,→}是一型,其中對于任意的a∈L,ar(a)=0,ar(→)=2,稱X上的自由T-代數為命題變元集合X上的格值命題演算系統的命題代數,記為LP(X)。以下格值命題邏輯系統LP(X)簡記為LP(X)。
定義2.3[4] 稱格值命題邏輯公式F為一極簡式,如果從F中去掉任何常元、文字或蘊涵式的出現,所得到的格值命題邏輯公式F*都不與F等值,簡記為ESF。
定義2.4[4] 稱格值命題邏輯公式F為不可分極簡式,如果F含有蘊涵詞且F是極簡式且不能表示為若干個格值命題邏輯公式的析取或合取,簡記為IESF。
定義2.5[4] LP(X)中的文字、常元和不可分極簡式統稱為廣義文字。
定義2.6[4](α-歸結)設α∈L,且廣義子句
G1=g1∨…∨gi∨…∨gm
G2=h1∨…∨hj∨…∨hn
如果gi ∧hj≤α,則稱
G= g1∨…∨gi-1∨gi+1∨…∨gm∨h1∨…∨hj-1∨hj+1∨…∨hn
為G1和G2的一個α-歸結,記為G=Resα( G1,G2),稱這里的gi與hj為一個α-歸結對,記為(gi, hj)-α,即gi, hj為α-歸結元。
定義2.7[4]設S={C1, C2, …, Cn}是LP(X)中的一個廣義子句集,α∈L,ω={D1, D2, …, Dm}稱為從S 到廣義子句Dm的α-歸結演繹,若
1) Di∈{C1, C2, …, Cn};或者: 2) 存在j, k
定義2.8 [4] 設S是LP(X)中的一個廣義子句集,若存在從S到空子句□的α-歸結演繹ω,則稱ω為S的一個否證或反駁。
定理2.1 [4] (可靠性)設S是LP(X)中的一個廣義子句集,若存在S的反駁ω,則S是α-不可滿足的。
定理2.2 [4] (弱完備性)設S是LP(X)中的一個正則的廣義子句集,α∈L,α
2 II-α-超歸結原理
定義3.1(II-α-超歸結)設α∈L,且廣義子句
Gi=gi1∨gi2∨…∨giti (i∈{1,2})
如果廣義子句G1存在廣義文字g11,g12,…,g1k,且G2中存在廣義文字g21,使得g1j∧g21≤α(j={1,2, …,k}),則稱
G= g1(k+1)∨…∨g1t1∨g22∨…∨g2t2
為廣義子句G1,G2的一個II-α-超歸結,記為G= ResIIα-H(G1, G2),稱這里的(g1j, g21) (j={1,2,…,k}為一個II-α-超歸結對,記為(g1j, g21) -αH -II。
定義3.2 設S={C1, C2,…,Cn}為LP(X)上的廣義子句集,且S=C1∧C2∧…∧ Cn,α∈L,ωIIα-H={D1,D2,…, Dm}稱為從S到廣義子句Dm的II-α-超歸結演繹,如果
1) Di∈{C1,C2,…, Cn},或者: 2) 存在j, k
定義3.3[4] 設C是LP(X)中的廣義子句,α∈L,v是LP(X)上的一個賦值,稱C是α-可滿足的,如果v(C)≥α;如果對LP(X)上任意的賦值v,v(C)≤α,則稱C是α-不可滿足的,即C是α-假。
定義3.4[4] 如果LP(X)中的廣義子句C是α-假,則稱C為α-空子句,簡記為α-□。
定義3.5 如果存在從S到α-□的II-α-超歸結演繹ωIIα-H,則稱ωIIα-H為II-αH-反駁。
定義3.6[4] 設S是LP(X)中一個子句集,α∈L,如果存在一個賦值v,使得v(S)≥α,則稱S是α-可滿足的;如果對LP(X)上任意的賦值 ,v(S)≤α,則稱S是α-不可滿足的。
定理3.1(II-α-超歸結原理可靠性)設S是LP(X)中的一個廣義子句集,若存在S的II-αH-反駁ωIIα-,則S是II-αH-不可滿足的。
證明 設ωIIα-H={D1, D2, …, Dm}為II-αH-反駁,設廣義子句G1中存在廣義文字g11,g12,…,g1k,且G2中存在廣義文字g21,則ResIIα-H(G1, G2)= g1(k+1)∨…∨g1t1∨g22∨…∨g2t2。事實上,該過程可分解為:
G3=Resα( G1,G2);G4=Resα( G3,G2) ;…;Gk-1=Resα( Gk-2,G2) ;Gk=Resα( Gk-1,G2)。
類似地,可以將ωIIα-H中的D1, D2, …, Dm分別進行分解。設Di(i=1,2,…,m)分解為D(i)1, D(i)2,…, D(i)ki,ki由每一步II-α-超歸結過程中II-α-超歸結對的個數而決定的。這樣我們就得到了ωIIα-H的分解序列:
D(1)1,D(1)2,…,D(1)k1-2,D(2)1,D(2)2,…,D(2)k2-2,…, D(m)1,D(m)2,…,D(m)km-2,
且D(m)km-2是α-□。這個序列就是通過對S實行α-歸結得到的演繹序列。由定理2.1知,S是α-不可滿足的。證畢。
定理3.2(II-α-超歸結原理弱完備性)設S是LP(X)中的一個正則的廣義子句集,α∈L,α
證明 已知S≤α,由定理2.1知,存在一個從S到α-□的α-歸結演繹ω。不妨設ω={D1, D2,…,Dm},若該演繹序列中存在Di , Di+1,…, Di+k (i,k={1,2,…,m})滿足如下條件:
Di+2 =Resα(Di, Di+1);Di+3 =Resα(Di, Di+2);…;Di+k =Resα(Di, Di+k-1);
根據定義3.1,則可將Di , Di+1,…, Di+k (i,k={1,2,…,m})用Di+k來替換。類似地,將ω={D1,D2,…,Dm}中滿足如上條件的序列進行替換,這樣我們就得到了一個新的歸結演繹序列ωIIα-H={D1, D2,…,Dl}。該序列即是一個從S到α-□的II-α-超歸結演繹。證畢。
3 舉例說明
下面我們給出一個具體的例子來說明II-α-超歸結原理的優越性。
例:S={C1,C2,C3,C4}是格值命題邏輯系統L9P(X)中的一個廣義子句集,L9P(X)是以L9={a1, a2,…,a9}為賦值域的邏輯系統,其中a1 首先我們基于格值命題邏輯系統LP(X)中的α-歸結原理對S進行驗證。 1) p 2) q 3) p′∨(p→a2)∨(r→s) 4) (q→a2)∨(α→q)′∨(r→q)′ ∨ (r→s)′ 5) (p→a2)∨(r→s)1)和3) 6) (r→s) 1)和5) 7) (α→q)′∨(r→q)′ ∨ (r→s)′2)和4) 8) (r→q)′ ∨ (r→s)′ 2)和7) 9) (r→s)′ 2)和8) 10) □6)和9) 現在我們基于格值命題邏輯系統LP(X)中的II-α-超歸結原理對S進行驗證。 1) p 2) q 3) p′∨(p→a2)∨(r→s) 4) (q→a2)∨(α→q)′∨(r→q)′ ∨ (r→s)′ 5) (r→s) 1)和3) 6) (r→s)′ 2)和4) 7) □ 5)和6) 在這個例子中,我們可以看出應用II-α-超歸結原理對S進行驗證時大大地減少了歸結過程的步數,也就是減少了歸結自動推理算法的運行時間,但卻沒有增加運算的復雜度,即沒有增加判斷兩個廣義文字是α-歸結對的次數。 5 結論 通過建立格值命題邏輯系統LP(X)上的II-α-超歸結原理理論,可以提高歸結自動推理算法的效率。尤其在實際問題中所涉及的α-歸結對非常多時,應用II-α-超歸結原理的優越性會更加明顯。 參考文獻: [1] 徐揚.格蘊涵代數[J].西南交通大學學報,1993,89(1):20-27. [2] Xu Yang, Qin Keyun. Lattice-valued propositional logic(Ⅰ)[J].Journal of Southwest Jiaotong University,1993, 1(2):123-128. [3] Qin Ke-yun, Xu Yang. Lattice-valued propositional logic(Ⅱ)[J].Journal of Southwest Jiaotong University,1994, 2(1):22-27. [4] Xu Yang, Ruan Da, Kerre E E, et al. α-resolution principle based on lattice-valued logic LP(X)[J]. Information Science, 2000, 1(30):195-223. [5] Meng Dan, Wang Xue-fang, Xu Yang, et al. Resolution based on six lattice-valued proposition logic L6P(X)[C]. IEEE International Conference on Systems, Man Cybernetics, 2003:2489-2494. [6] Wang Wei, Jiang Bao-qing, Xu Yang. α-automated reasoning method based on LP(X)[C]// FLINS 2004 6th International Conference on Applied Computational Intelligence[C]. Bankenberghe: World Scientific Press, 2004: 105-110. [7] Qiu Xiao-ping, Li Hai-ming, Du Yajun, et al. Adding Forecast Support to Workflow Management System by Classical Logic Formula Computing[C], Proceedings of the second international conference on machine learning and cybernetics(ICMLC'2003),2003(4):2061-2066. [8] 李曉冰,邱小平,徐揚.格值命題邏輯系統L(2n+1)P(X)中基于半正則廣義文字的自動推理算法[J].模糊系統與數學,2009,23(4):21-26. [9] 李曉冰,邱小平,徐揚.格值命題邏輯系統L9P(X)中的自動推理算法[J].計算機工程與應用,2008,44(10):6-9. [10] 李曉冰.基于語言真值格值邏輯的歸結自動推理研究[D].西南交通大學博士學位論文,2008.