智能主體的信念認(rèn)知時態(tài)子結(jié)構(gòu)邏輯模型

　　0 引言

　　為適應(yīng)環(huán)境變化和協(xié)作求解,智能主體(agent)必須利用知識修改內(nèi)部狀態(tài),即心智狀態(tài)(mental state)。主體的心智狀態(tài)為主體如何行動提供了一種解釋,也就是說主體的行動是由主體的心智狀態(tài)驅(qū)動的,如認(rèn)知、情感、意向等。邏輯是描述主體心智狀態(tài)的重要工具[1]。1990年,Moore[2]使用形式邏輯對主體進(jìn)行了建模,并主要研究了主體擁有的知識與實現(xiàn)的動作之間的關(guān)系;隨后Cohen等人[3]系統(tǒng)地研究了信念、目標(biāo)、持續(xù)目標(biāo)、意圖和理性的邏輯表達(dá)和演算問題,他們的工作基于線性時態(tài)邏輯,在語義上則以Kripke可能世界語義學(xué)為基礎(chǔ),并給出了BDI形式模型;其后,Rao等人[4]提出了理想agent的BDI模型,使用了三個基本的模態(tài)算符:信念(belief)、愿望(desire)和意圖(intention)建立了主體的BDI模型;Jiao等人[5]針對主體是在進(jìn)程級運行的程序,運用π演算描述了主體的理性和行為意圖,利用π演算這種刻畫通信系統(tǒng)的進(jìn)程演算表示出主體間的交互;胡山立等人[6,7]在真假子集語義基礎(chǔ)上通過對模型的代數(shù)結(jié)構(gòu)施加一定的約束,開發(fā)了雙子集語義改進(jìn)模型,避免了基于正規(guī)模態(tài)邏輯表示的邏輯全知問題以及由此帶來的副作用等問題。此外,Konolige等人[8~13]也做了相關(guān)值得肯定的工作,遍及BDI理論研究與應(yīng)用的多個領(lǐng)域職稱論文。

　　盡管BDI或類BDI模型已成為研究智能主體理論模型的主要工具,但這些模型仍普遍存在下述的一些問題:

　　a)主體理論模型中普遍存在邏輯全知(logic omniscience)[1]。

　　b)重視主體間知識交互,而輕視主體內(nèi)部知識或狀態(tài)。

　　c)由經(jīng)典模態(tài)邏輯或二值邏輯引起的理論模型對真實世界的刻畫粗精度。

　　基于此,本文針對上述問題進(jìn)行了相關(guān)研究,并將研究工作聚焦于智能主體的信念,針對其作出了相關(guān)邏輯模型。考慮到對于愿望和意圖,不同的應(yīng)用和應(yīng)用觀對其有不同的看法和定義,因此本文并未進(jìn)行深入研究,只著重刻畫了認(rèn)知和決策的關(guān)鍵,即信念。

　　1 智能主體信念的形成與表示

　　1.1 智能主體信念的形成及其問題

　　無論是BDI模型還是其他的智能主體的理論模型,對于信念的形成與表示都是建模的基礎(chǔ)。但是在當(dāng)前的許多理論模型中,對信念的形成存在一定的問題。例如,作為經(jīng)典的模型,在Rao等人[4]的模型中,在建模時雖使用到時態(tài)邏輯模型及其技巧,但僅考慮到系統(tǒng)的未來狀態(tài),而不關(guān)注過去的認(rèn)知。實際上,造成類似的問題主要在于其對信念(知識)的獲取僅考慮與外部主體進(jìn)行交互,而輕視了主體在過去的知識。

　　事實上,作為一個智能主體,其獲取信念(知識)的途徑主要有兩種:a)他省(extrospectiveness),即通過外界交互,從其他主體中獲取信息;b)自省(introspectiveness),即通過自己的歷史數(shù)據(jù)庫獲取相關(guān)知識的信息。因此,對于主體信念的描述與刻畫,兩種途徑缺一不可。在當(dāng)前研究中,體現(xiàn)他省的BDI模型較多,卻較少帶自省功能的模型。但從時態(tài)數(shù)據(jù)庫、時態(tài)知識庫的角度看,智能主體的知識也是一個隨著時間軸向前推進(jìn)的歷史數(shù)據(jù)庫序列H=(H?0,…,H?n,Hn+1,…),在不同的階段有不同的知識集,這些知識集對當(dāng)前信念的建立影響巨大,自省不可忽視。因此,在邏輯建模中,必須體現(xiàn)他省和自省,并處理其間的各類知識沖突。

　　考慮到主體理論模型中普遍存在邏輯全知的問題,這也主要是因為相關(guān)模型使用了經(jīng)典模態(tài)邏輯(或相關(guān)變形系統(tǒng))、二值邏輯導(dǎo)致的結(jié)果。邏輯全知問題主要包括兩個方面:

　　a)一個主體如果知道一個命題,那么它知道它所知道的命題的全部邏輯后承。

　　b)一個主體知道所有的真理(重言式)。

　　造成問題a)是因為理論模型采用了形如經(jīng)典模態(tài)邏輯中的K公理式的內(nèi)定理。造成問題b)的主要原因有兩點:第一點是因為理論模型采用了形如經(jīng)典模態(tài)邏輯中的RN規(guī)則式的規(guī)則造成;第二點是在計算科學(xué),尤其是在機群協(xié)同工作下的智能主體的認(rèn)知過程不應(yīng)存在所謂的“重言式”模式的內(nèi)定理,所有公式的成立與否都應(yīng)采用構(gòu)造性證明進(jìn)行論證,而非傳統(tǒng)的二值邏輯形式及其粗精度刻畫。

　　1.2 “雙省”智能主體的信念表示

　　基于上述問題,本文提出了相應(yīng)的解決方法。首先,主體的信念必須與他省和自省相結(jié)合。具體體現(xiàn)在不僅重視交互,而且重視歷史數(shù)據(jù)。由此在表意上,可以使用Bel(k)=KHφ表示主體k在當(dāng)前時刻具有信念φ。其中:K表示“知道”算子,體現(xiàn)了他省;H仍使用時態(tài)邏輯中的標(biāo)記意義,表示“在此之前一直……(不包括當(dāng)前時間)”,體現(xiàn)了自省,只有當(dāng)他省和自省都為“必然”時,知識才能成為信念。其次,要解決邏輯全知與非構(gòu)造性語義的粗精度刻畫問題,一種可行的方式是使用子結(jié)構(gòu)邏輯(substructural logics)。根據(jù)子結(jié)構(gòu)邏輯的構(gòu)造性證明,能有效避免上述問題,并可通過結(jié)構(gòu)規(guī)則的增刪,修改傳統(tǒng)Hilbert風(fēng)格的邏輯演算所固留的諸如單調(diào)性、收縮性等弊病,以增加系統(tǒng)的可計算性。

　　據(jù)此,可建立相應(yīng)的認(rèn)知時態(tài)子結(jié)構(gòu)邏輯系統(tǒng)。鑒于其表示了智能主體的信念,同時采用的是認(rèn)知邏輯、時態(tài)邏輯和子結(jié)構(gòu)演算的綜合解決方法,本文將新的系統(tǒng)稱為BSoET系統(tǒng),意為substructural logic of epistemic and temporality in belief。在下一部分,將對系統(tǒng)作詳細(xì)介紹。

　　2 BSoET及其Gentzen系統(tǒng)

　　2.1 可能世界與可達(dá)關(guān)系

　　首先考慮到系統(tǒng)需要做到他省和自省,必須對認(rèn)知的可能世界與可達(dá)關(guān)系作出定義,這種定義是針對框架的(frame)。

　　定義1 他省框架。一個他省框架是一個二元組?F=〈T,R?e〉。其中:T為時間結(jié)構(gòu)的集合,對于每一個T?i∈T,T?i表示一個時間結(jié)構(gòu);R?e為時間結(jié)構(gòu)間的一個自反和傳遞的可達(dá)?關(guān)系。

　　直觀上,對于每一個T?i∈T,T?i表示一個智能主體。這是考慮到每個智能主體都有一個歷史數(shù)據(jù)庫,可以用T?i表示歷史數(shù)據(jù)庫(H?0,…,H?n,Hn+1,…)的集合。在拓?fù)湫问缴?可將T?i理解為一個時間軸,軸上的點表示了主體在該時刻上的歷史數(shù)據(jù)。由此,能進(jìn)一步定義自省框架。

　　定義2 自省框架。一個自省框架是一個二元組T=〈T,R?t〉。其中:T為時間點的集合,R?t為一個時間點間的一個傳遞可達(dá)關(guān)系。

　　假定不同軸的同一時刻的時間點之間的可達(dá)關(guān)系與時間軸之間的可達(dá)關(guān)系是一致的,據(jù)定義1和2,可以將兩個框架合并。

　　定義3 他省且自省框架。一個他省且自省框架為一個三元組F=〈T,R?e,R?t〉。其中:T為時間點的集合;R?e為一個自反和傳遞的可達(dá)關(guān)系;R?t為一個傳遞可達(dá)關(guān)系。

　　其示意如圖1所示。

　　直觀上T上的點通過R?t關(guān)系,構(gòu)成各條時間軸,每條時間軸代表一個主體(及其歷史數(shù)據(jù)庫),表示了自省關(guān)系;不同軸的同一時刻的時間點通過R?e,構(gòu)成了他省關(guān)系。

　　另一方面,作為他省關(guān)系,R?e為一個自反和傳遞的可達(dá)關(guān)系對于傳統(tǒng)BDI模型的認(rèn)知可達(dá)關(guān)系是一般的;而作為自省關(guān)系,R?t不能具有自反性。在直觀上,人的自省總是反省過去,對于現(xiàn)在是無法反省的,而作為他省關(guān)系的R?e的自反性,則主要體現(xiàn)了主體對自我知識集的認(rèn)知,因此需要保留。

　　在沒有具體解釋框架語義之前,針對R?e和R?t關(guān)系,分別用模態(tài)算子?□•和□對應(yīng)它們類似于經(jīng)典模態(tài)邏輯的必然關(guān)系,并由此用?□•□φ來表示一個主體有信念φ,假設(shè)這個主體是k,可以將其簡記為Bel(k)=?□•□φ。

　　2.2 Gentzen系統(tǒng)

　　據(jù)上,本文將對他省和自省框架構(gòu)造子結(jié)構(gòu)演算系統(tǒng),為體現(xiàn)子結(jié)構(gòu)演算特點,在此用Gentzen風(fēng)格的演算系統(tǒng)(由德國人Gentzen 1934年在其博士畢業(yè)論文中提出的一種邏輯演算,國內(nèi)也翻譯為相繼式演算,但更多直譯為Gentzen演算,在該演算中分為結(jié)構(gòu)規(guī)則和運算規(guī)則,運算規(guī)則又分為左規(guī)則和右規(guī)則,是有別于Hilbert風(fēng)格的自然演繹方法的構(gòu)造性邏輯演算方法,主要用于證明論)來構(gòu)造BSoET,系統(tǒng)如下:

　　公理:A?A

　　結(jié)構(gòu)規(guī)則:

　　X├AY,A,Z├BY,X,Z├B(Cut)

　　*X├AX├A(T for ?□•) *X├A**X├A(4 for ?□•) ○X├A○○X├A(4 for □)

　　運算規(guī)則:

　　X,A,Y├CX,A∧B,Y├C(∧L)

　　X,B,Y├CX,A∧B,Y├C(∧L)

　　X├A X├BX├A∧B(∧R)

　　X,A,Y├C X,B,Y├CX,A∨B,Y├C(∨L)

　　X├AX├A∨B(∨R)

　　X├BX├A∨B(∨R)

　　X,A,Y,B,Z├CY,X,A→B,Z├C(→L) X,A├BX├B(→R)

　　X,A,Y├BX,*?□•A,Y├B(?□•L) *X├AX├?□•A(?□•R)?X,A,Y├BX,○□A,Y├B(□L) ○X├AX├□A(□R)

　　在此,“,”“*”“○”分別是三個不同的punc mark(句法標(biāo)記,非算符)。其中“,”是一個無序的句法結(jié)構(gòu)標(biāo)記,它分割了多個參與演算的公式序列;而“*”和“○”分別是□•和□的punc mark[14]。其中結(jié)構(gòu)規(guī)則“T for □•”表明了如果公式序列X能在“*”的演繹下得到A,則在一般演繹下也能得到A,這恰好對應(yīng)了R?e關(guān)系的自反性。類似地,結(jié)構(gòu)規(guī)則“4 for □•”對應(yīng)了R?e關(guān)系的傳遞性,結(jié)構(gòu)規(guī)則“4 for □”對應(yīng)了R?t關(guān)系的傳遞性。

　　注意到,這是一個典型的“直覺主義”邏輯系統(tǒng),是基于構(gòu)造性證明的。同時由于類似K公理和RN規(guī)則的內(nèi)定理不存在于BSoET的結(jié)構(gòu)規(guī)則中,也有效避免了邏輯全知問題。值得一提的是,由于“∧L”規(guī)則的存在,系統(tǒng)實際保留了Weakening規(guī)則,即該系統(tǒng)的推理仍然是單調(diào)的。同時由于punc mark“,”的無序性,交換律也依然保持其有效性,但系統(tǒng)不具有收縮規(guī)則,避免了運算資源的可重用性[15]。

　　另一方面,在BSoET系統(tǒng)中,本文也沒有考慮算子“┐”,其主要原因是BSoET系統(tǒng)是一個直覺主義邏輯系統(tǒng),其證明為構(gòu)造性證明。由此,構(gòu)造一個┐φ的信念與構(gòu)造一個φ的信念的工作是相似的。

　　3 BSoET系統(tǒng)的語義模型

　　定義4 點集與命題[14]。一個點集P=〈P,〉為集合P及其上的偏序關(guān)系。P上的命題集Prop(T)為P上的所有向上封閉的子集X,即若x∈X且xx’,則x’∈X。

　　定義5 可達(dá)關(guān)系。

　　1)二元關(guān)系R為點集P上的二元關(guān)系當(dāng)且僅當(dāng)對?x,y∈P,如果xSy且?x’(x’x),則?y’(y’y),使得x’Ry’。類似地,如果xRy且?y’(y’y),則?x’(x’x),使得x’Ry’。

　　2)二元關(guān)系R為點集P上的豐滿的(plump)二元關(guān)系,當(dāng)且僅當(dāng)對于?x, y, x’, y’∈P,如果xRy且x’x,y’y,則x’Ry’。

　　定義6 框架及框架關(guān)系。一個框架F為一點集P及其上的二元可達(dá)關(guān)系,寫做F=〈P,R?e,R?t〉。其中R?e和R?t分別為他省和自省的二元關(guān)系。

　　定義7 框架賦值。

　　1){x∈F:x?p}∈Prop{F};

　　2)x?A∧B iff ?x∈F, x?A且x?B;

　　3)x?A∨B iff ?x∈F, x?A或x?B;

　　4)x?□•A iff ?y∈F,如果x R?e y,則y?A;

　　5)x?□A iff ?y∈F,如果x R?t y,則y?A。

　　定義8 衍推。

　　1)稱X相對于模型M衍推A,記做“X├?MA”,當(dāng)且僅當(dāng)對?x∈M,如果x?X,則x?A;

　　2)稱X相對于框架F衍推A,記做“X├?FA”,當(dāng)且僅當(dāng)對?M∈F,X├?MA;

　　3)稱X相對于框架類F衍推A,記做“X├?F A”,當(dāng)且僅當(dāng)對?F∈F,X├?FA。

　　由此易證得以下定理,限于篇幅證明從略,有興趣的讀者可以參見文獻(xiàn)[16]。

　　定理1 可靠性定理。BSoET系統(tǒng)相對于框架條件為xR?e x、xR?e y∧yR?e z→xR?e z和xR?t y∧yR?t z→xR?t z的框架是可靠的。

　　定理2 完全性定理。BSoET系統(tǒng)相對于框架條件為xR?e x、xR?e y∧yRe z→xR?e z和xR?t y∧yR?t z→xR?t z的框架是完全的。

　　4 群體信念與公共信念

　　在BSoET系統(tǒng)中,主體k形成的信念可由Bel(k)=?□•□φ表達(dá),其不僅考慮了主體之間的他省,還考慮了參與認(rèn)知主體的自省,體現(xiàn)了只有當(dāng)他省和自省都為“必然”時,知識才能成為信念的觀點——主體k擁有信念φ的原因不僅僅是因為當(dāng)前狀態(tài)下與外界主體的通過交互獲得知識,更要考慮其歷史?數(shù)據(jù)。

　　基于BSoET系統(tǒng),易得在群體認(rèn)知中的群體信念“Eφ” (everyone has the belief φ)與公共信念“Cφ” (it is common belief that φ),對于n個智能體,其定義如下:

　　Eφ=Bel(1)∧…∧Bel(n)=□•?1□?1φ∧…∧□•?n□?nφ;

　　Cφ=φ∧Eφ∧EEφ∧…= ∧i≥0E?iφ

　　5 結(jié)束語

　　本文針對智能主體的“雙省”信念及其形成與表示進(jìn)行了相關(guān)研究,采用了認(rèn)知時態(tài)子結(jié)構(gòu)邏輯建模的方法,表達(dá)了智能主體獲得“雙省”信念的方式,針對其建立了相應(yīng)的邏輯系統(tǒng)BSoET。由于BSoET系統(tǒng)采用的是子結(jié)構(gòu)演算,有效避免了邏輯全知問題,其模型語義與構(gòu)造性證明方法較經(jīng)典二值邏輯更細(xì)精度地刻畫了信念的形成。

　　在BSoET系統(tǒng)中討論R?e和R?t關(guān)系時,本文主要討論了它們的必然算子,即□•和□。對于□•和□的對偶算子◇•和◇在本文中并沒有討論,不討論其的主要原因在于◇•和◇算子不是信念形成的關(guān)鍵,同時也對愿望和意圖不起關(guān)鍵作用。因此,在下一步工作中的研究重點在于,如何將R?e擴(kuò)充為動作和動態(tài)關(guān)系,如將算子□•擴(kuò)充為[α]或[α]?n,又如何進(jìn)一步在子結(jié)構(gòu)演算中豐富R?t關(guān)系,使其進(jìn)一步具有線性、序列性、非分支性和有窮間隔性等性質(zhì)。同時,還可以通過添加相應(yīng)的表示將來狀態(tài)的算子“■”,由相關(guān)領(lǐng)域的研究人員形成相應(yīng)的愿望、意圖和BDI模型,并最后付諸領(lǐng)域應(yīng)用。

《智能主體的信念認(rèn)知時態(tài)子結(jié)構(gòu)邏輯模型》

上一篇：淺談加強計算機網(wǎng)絡(luò)安全的防范對策

下一篇：分析計算機網(wǎng)絡(luò)系統(tǒng)在制堿工業(yè)中的應(yīng)用