智能主體的信念認(rèn)知時態(tài)子結(jié)構(gòu)邏輯模型
若水221147由 分享
時間：
摘 要:智能主體獲取信念的途徑主要有兩種:一種為他省,通過外界交互,從其他主體獲取信息;另一種為自省,通過自己的歷史數(shù)據(jù)庫獲取相關(guān)知識。對于主體信念的描述及刻畫,兩種途徑缺一不可,但當(dāng)前的BDI理論模型中較多地為他省系統(tǒng),沒有做到兩者相結(jié)合。其次,在當(dāng)前的許多理論模型中,通常使用的是二值邏輯、經(jīng)典模態(tài)邏輯或其變形系統(tǒng),使得相應(yīng)的邏輯系統(tǒng)普遍存在邏輯全知和粗精度刻畫等問題。針對上述問題進(jìn)行了探討,采用了認(rèn)知時態(tài)子結(jié)構(gòu)邏輯建模的方法,表達(dá)了智能主體獲得“雙省”信念的方式,針對其建立了相應(yīng)的邏輯系統(tǒng)BSoET。
關(guān)鍵詞:智能主體;信念;自省;他省;認(rèn)知時態(tài)子結(jié)構(gòu)邏輯
Substructural logic of epistemic and temporality in belief of agent
LIU Dong-ning?1,TANG Yong?2
(1.School of Computer, Guangdong University of Technology, Guangzhou 510006, China;2.School of Computer, South China Normal University, Guangzhou 510631, China)
Abstract:There are two kinds of approach to get belief as an agent. One is extrospectiveness, which gets information from other body through outside interaction. The other is introspectiveness, which gets information from own history database. The two ways are indispensable to describe belief of agent. However, nowadays BDI logics mostly use extrospectiveness, not combination of extrospectiveness and introspectiveness. Also, most BDI logics are usually based two-value logic, classical modal logic or its transmutation, which makes many logic systems have problems such as logic omniscience and coarse depiction.For these problems, this paper made some research and put forward a substructural logic of epistemic and temporality(BSoET)focusing as belief of agent.
Key words:agent; belief; introspectiveness; extrospectiveness; substructural logic of epistemic and temporality
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擴充為動作和動態(tài)關(guān)系,如將算子□•擴充為[α]或[α]?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)用。
參考文獻(xiàn):
[1]史忠植.智能主體及其應(yīng)用[M].北京:科學(xué)出版社,2000:12-22.
[2]MOORE R C.A formal theory of knowledge and action[M]//Formal Theories of the Commonsense World.[S.l.]:Ablex Publishing Corperation,1985:319-358.
[3]COHEN P R,LEVESQUE H J.Intention is choice with commitment[J].Artificial Intelligence,1990,42(2-3):213-261.
[4]RAO A S,GEORGEFF M P.Deliberation and intentions,Technical Notes 10[R].[S.l.]:Australian Artificial Intelligence Institute,1991.
[5]JIAO Wen-ping,SHI Zhong-zhi.Formalizing agent’s attitudes with polyadic π-calculus[C]//Proc of the 4th Workshop on Practical Reasoning and Rationality.Stockholm:[s.n.],1999:21-27.
[6]胡山立,石純一.Agent意圖的雙子集語義改進(jìn)模型[J].軟件學(xué)報,2006,17(3):396-402.
[7]HU Shan-li,SHI Chun-yi.An improved twin-subset semantic model for intention of agent[J].Journal of Software,2006,17(3):?396-402.
[8]KONOLIGE K,POLLACK M E.A representationalist theory of intention[C]//Proc of IJCAI’93.1993:390-395.
[9]SINGH M P.Multiagent systems:a theoretical framework for intentions,know-how,and communications[C]//Lecture Notes in Artificial Intelligence.[S.l.]:Springer,1994.
[10] NAIR V C P.On extending BDI logics[D].Queensland:Griffith University,2003.
[11]RAFAEL H B,MEHDI D,J?RGEN D,et al.Multi-agent programming:languages,platforms and applications[M].Berlin:[s.n.],2005.
[12]RAFAEL H B,MICHAEL F,WILLEM V,et al.Verifying multi-agent programs by model checking[J].Journal of Autonomous Agents and Multi-Agent Systems,2006,12(2):239-256.
[13]RAFAEL H B,JOMI F H,MICHAEL W.Programming multi-agent systems in AgentSpeak using Jason[M]//[S.l.]:Wiley,2007.
[14]RESTALL G.An introduction to substructural logics[M].Routledge,Tokyo:Mathematical Society of Japan,2000.
[15]ONO H.Proof-theoretic methods in nonclassical logics[R].1998:207-254.
[16]劉冬寧.時態(tài)信息處理中若干問題的邏輯公理化研究[R].廣州:中山大學(xué),2009.
[17]CAMILO T.The BDI model of agency and BDI logics[R].2005.
[18]BULLING N.Modal logics for games, time, and beliefs[D].[S.l.]:Clausthal University of Technology,2006.
關(guān)鍵詞:智能主體;信念;自省;他省;認(rèn)知時態(tài)子結(jié)構(gòu)邏輯
Substructural logic of epistemic and temporality in belief of agent
LIU Dong-ning?1,TANG Yong?2
(1.School of Computer, Guangdong University of Technology, Guangzhou 510006, China;2.School of Computer, South China Normal University, Guangzhou 510631, China)
Abstract:There are two kinds of approach to get belief as an agent. One is extrospectiveness, which gets information from other body through outside interaction. The other is introspectiveness, which gets information from own history database. The two ways are indispensable to describe belief of agent. However, nowadays BDI logics mostly use extrospectiveness, not combination of extrospectiveness and introspectiveness. Also, most BDI logics are usually based two-value logic, classical modal logic or its transmutation, which makes many logic systems have problems such as logic omniscience and coarse depiction.For these problems, this paper made some research and put forward a substructural logic of epistemic and temporality(BSoET)focusing as belief of agent.
Key words:agent; belief; introspectiveness; extrospectiveness; substructural logic of epistemic and temporality
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擴充為動作和動態(tài)關(guān)系,如將算子□•擴充為[α]或[α]?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)用。
參考文獻(xiàn):
[1]史忠植.智能主體及其應(yīng)用[M].北京:科學(xué)出版社,2000:12-22.
[2]MOORE R C.A formal theory of knowledge and action[M]//Formal Theories of the Commonsense World.[S.l.]:Ablex Publishing Corperation,1985:319-358.
[3]COHEN P R,LEVESQUE H J.Intention is choice with commitment[J].Artificial Intelligence,1990,42(2-3):213-261.
[4]RAO A S,GEORGEFF M P.Deliberation and intentions,Technical Notes 10[R].[S.l.]:Australian Artificial Intelligence Institute,1991.
[5]JIAO Wen-ping,SHI Zhong-zhi.Formalizing agent’s attitudes with polyadic π-calculus[C]//Proc of the 4th Workshop on Practical Reasoning and Rationality.Stockholm:[s.n.],1999:21-27.
[6]胡山立,石純一.Agent意圖的雙子集語義改進(jìn)模型[J].軟件學(xué)報,2006,17(3):396-402.
[7]HU Shan-li,SHI Chun-yi.An improved twin-subset semantic model for intention of agent[J].Journal of Software,2006,17(3):?396-402.
[8]KONOLIGE K,POLLACK M E.A representationalist theory of intention[C]//Proc of IJCAI’93.1993:390-395.
[9]SINGH M P.Multiagent systems:a theoretical framework for intentions,know-how,and communications[C]//Lecture Notes in Artificial Intelligence.[S.l.]:Springer,1994.
[10] NAIR V C P.On extending BDI logics[D].Queensland:Griffith University,2003.
[11]RAFAEL H B,MEHDI D,J?RGEN D,et al.Multi-agent programming:languages,platforms and applications[M].Berlin:[s.n.],2005.
[12]RAFAEL H B,MICHAEL F,WILLEM V,et al.Verifying multi-agent programs by model checking[J].Journal of Autonomous Agents and Multi-Agent Systems,2006,12(2):239-256.
[13]RAFAEL H B,JOMI F H,MICHAEL W.Programming multi-agent systems in AgentSpeak using Jason[M]//[S.l.]:Wiley,2007.
[14]RESTALL G.An introduction to substructural logics[M].Routledge,Tokyo:Mathematical Society of Japan,2000.
[15]ONO H.Proof-theoretic methods in nonclassical logics[R].1998:207-254.
[16]劉冬寧.時態(tài)信息處理中若干問題的邏輯公理化研究[R].廣州:中山大學(xué),2009.
[17]CAMILO T.The BDI model of agency and BDI logics[R].2005.
[18]BULLING N.Modal logics for games, time, and beliefs[D].[S.l.]:Clausthal University of Technology,2006.