摘 要:智能主體獲取信念的途徑主要有兩種:一種為他省,通過外界交互,從其他主體獲取信息;另一種為自省,通過自己的歷史數(shù)據(jù)庫獲取相關(guān)知識(shí)。對(duì)于主體信念的描述及刻畫,兩種途徑缺一不可,但當(dāng)前的BDI理論模型中較多地為他省系統(tǒng),沒有做到兩者相結(jié)合。其次,在當(dāng)前的許多理論模型中,通常使用的是二值邏輯、經(jīng)典模態(tài)邏輯或其變形系統(tǒng),使得相應(yīng)的邏輯系統(tǒng)普遍存在邏輯全知和粗精度刻畫等問題。針對(duì)上述問題進(jìn)行了探討,采用了認(rèn)知時(shí)態(tài)子結(jié)構(gòu)邏輯建模的方法,表達(dá)了智能主體獲得“雙省”信念的方式,針對(duì)其建立了相應(yīng)的邏輯系統(tǒng)BSoET。
　　關(guān)鍵詞:智能主體;信念;自省;他省;認(rèn)知時(shí)態(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)必須利用知識(shí)修改內(nèi)部狀態(tài),即心智狀態(tài)(mental state)。主體的心智狀態(tài)為主體如何行動(dòng)提供了一種解釋,也就是說主體的行動(dòng)是由主體的心智狀態(tài)驅(qū)動(dòng)的,如認(rèn)知、情感、意向等。邏輯是描述主體心智狀態(tài)的重要工具`1`。1990年,Moore`2`使用形式邏輯對(duì)主體進(jìn)行了建模,并主要研究了主體擁有的知識(shí)與實(shí)現(xiàn)的動(dòng)作之間的關(guān)系;隨后Cohen等人`3`系統(tǒng)地研究了信念、目標(biāo)、持續(xù)目標(biāo)、意圖和理性的邏輯表達(dá)和演算問題,他們的工作基于線性時(shí)態(tài)邏輯,在語義上則以Kripke可能世界語義學(xué)為基礎(chǔ),并給出了BDI形式模型;其后,Rao等人`4`提出了理想agent的BDI模型,使用了三個(gè)基本的模態(tài)算符:信念(belief)、愿望(desire)和意圖(intention)建立了主體的BDI模型;Jiao等人`5`針對(duì)主體是在進(jìn)程級(jí)運(yùn)行的程序,運(yùn)用π演算描述了主體的理性和行為意圖,利用π演算這種刻畫通信系統(tǒng)的進(jìn)程演算表示出主體間的交互;胡山立等人`6,7`在真假子集語義基礎(chǔ)上通過對(duì)模型的代數(shù)結(jié)構(gòu)施加一定的約束,開發(fā)了雙子集語義改進(jìn)模型,避免了基于正規(guī)模態(tài)邏輯表示的邏輯全知問題以及由此帶來的副作用等問題。此外,Konolige等人`8~13`也做了相關(guān)值得肯定的工作,遍及BDI理論研究與應(yīng)用的多個(gè)領(lǐng)域職稱論文。
　　盡管BDI或類BDI模型已成為研究智能主體理論模型的主要工具,但這些模型仍普遍存在下述的一些問題:
　　a)主體理論模型中普遍存在邏輯全知(logic omniscience)`1`。
　　b)重視主體間知識(shí)交互,而輕視主體內(nèi)部知識(shí)或狀態(tài)。
　　c)由經(jīng)典模態(tài)邏輯或二值邏輯引起的理論模型對(duì)真實(shí)世界的刻畫粗精度。
　　基于此,本文針對(duì)上述問題進(jìn)行了相關(guān)研究,并將研究工作聚焦于智能主體的信念,針對(duì)其作出了相關(guān)邏輯模型?？紤]到對(duì)于愿望和意圖,不同的應(yīng)用和應(yīng)用觀對(duì)其有不同的看法和定義,因此本文并未進(jìn)行深入研究,只著重刻畫了認(rèn)知和決策的關(guān)鍵,即信念。
　　
　　1 智能主體信念的形成與表示
　　1.1 智能主體信念的形成及其問題
　　無論是BDI模型還是其他的智能主體的理論模型,對(duì)于信念的形成與表示都是建模的基礎(chǔ)。但是在當(dāng)前的許多理論模型中,對(duì)信念的形成存在一定的問題。例如,作為經(jīng)典的模型,在Rao等人`4`的模型中,在建模時(shí)雖使用到時(shí)態(tài)邏輯模型及其技巧,但僅考慮到系統(tǒng)的未來狀態(tài),而不關(guān)注過去的認(rèn)知。實(shí)際上,造成類似的問題主要在于其對(duì)信念(知識(shí))的獲取僅考慮與外部主體進(jìn)行交互,而輕視了主體在過去的知識(shí)。
　　
　　事實(shí)上,作為一個(gè)智能主體,其獲取信念(知識(shí))的途徑主要有兩種:a)他省(extrospectiveness),即通過外界交互,從其他主體中獲取信息;b)自省(introspectiveness),即通過自己的歷史數(shù)據(jù)庫獲取相關(guān)知識(shí)的信息。因此,對(duì)于主體信念的描述與刻畫,兩種途徑缺一不可。在當(dāng)前研究中,體現(xiàn)他省的BDI模型較多,卻較少帶自省功能的模型。但從時(shí)態(tài)數(shù)據(jù)庫、時(shí)態(tài)知識(shí)庫的角度看,智能主體的知識(shí)也是一個(gè)隨著時(shí)間軸向前推進(jìn)的歷史數(shù)據(jù)庫序列H=(H?0,…,H?n,Hn+1,…),在不同的階段有不同的知識(shí)集,這些知識(shí)集對(duì)當(dāng)前信念的建立影響巨大,自省不可忽視。因此,在邏輯建模中,必須體現(xiàn)他省和自省,并處理其間的各類知識(shí)沖突。
　　
　　考慮到主體理論模型中普遍存在邏輯全知的問題,這也主要是因?yàn)橄嚓P(guān)模型使用了經(jīng)典模態(tài)邏輯(或相關(guān)變形系統(tǒng))、二值邏輯導(dǎo)致的結(jié)果。邏輯全知問題主要包括兩個(gè)方面:
　　a)一個(gè)主體如果知道一個(gè)命題,那么它知道它所知道的命題的全部邏輯后承。
　　b)一個(gè)主體知道所有的真理(重言式)。
　　
　　造成問題a)是因?yàn)槔碚撃Ｐ筒捎昧诵稳缃?jīng)典模態(tài)邏輯中的K公理式的內(nèi)定理。造成問題b)的主要原因有兩點(diǎn):第一點(diǎn)是因?yàn)槔碚撃Ｐ筒捎昧诵稳缃?jīng)典模態(tài)邏輯中的RN規(guī)則式的規(guī)則造成;第二點(diǎn)是在計(jì)算科學(xué),尤其是在機(jī)群協(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)前時(shí)刻具有信念φ。其中:K表示“知道”算子,體現(xiàn)了他省;H仍使用時(shí)態(tài)邏輯中的標(biāo)記意義,表示“在此之前一直……(不包括當(dāng)前時(shí)間)”,體現(xiàn)了自省,只有當(dāng)他省和自省都為“必然”時(shí),知識(shí)才能成為信念。其次,要解決邏輯全知與非構(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ì)算性。
　　
　　據(jù)此,可建立相應(yīng)的認(rèn)知時(shí)態(tài)子結(jié)構(gòu)邏輯系統(tǒng)。鑒于其表示了智能主體的信念,同時(shí)采用的是認(rèn)知邏輯、時(shí)態(tài)邏輯和子結(jié)構(gòu)演算的綜合解決方法,本文將新的系統(tǒng)稱為BSoET系統(tǒng),意為substructural logic of epistemic and temporality in belief。在下一部分,將對(duì)系統(tǒng)作詳細(xì)介紹。
　　2 BSoET及其Gentzen系統(tǒng)
　　2.1 可能世界與可達(dá)關(guān)系
　　
　　首先考慮到系統(tǒng)需要做到他省和自省,必須對(duì)認(rèn)知的可能世界與可達(dá)關(guān)系作出定義,這種定義是針對(duì)框架的(frame)。 　
　　定義1 他省框架。一個(gè)他省框架是一個(gè)二元組?F=〈T,R?e〉。其中:T為時(shí)間結(jié)構(gòu)的集合,對(duì)于每一個(gè)T?i∈T,T?i表示一個(gè)時(shí)間結(jié)構(gòu);R?e為時(shí)間結(jié)構(gòu)間的一個(gè)自反和傳遞的可達(dá)?關(guān)系。 　　
　　直觀上,對(duì)于每一個(gè)T?i∈T,T?i表示一個(gè)智能主體。這是考慮到每個(gè)智能主體都有一個(gè)歷史數(shù)據(jù)庫,可以用T?i表示歷史數(shù)據(jù)庫(H?0,…,H?n,Hn+1,…)的集合。在拓?fù)湫问缴?可將T?i理解為一個(gè)時(shí)間軸,軸上的點(diǎn)表示了主體在該時(shí)刻上的歷史數(shù)據(jù)。由此,能進(jìn)一步定義自省框架。
　　
　　定義2 自省框架。一個(gè)自省框架是一個(gè)二元組T=〈T,R?t〉。其中:T為時(shí)間點(diǎn)的集合,R?t為一個(gè)時(shí)間點(diǎn)間的一個(gè)傳遞可達(dá)關(guān)系。
　　假定不同軸的同一時(shí)刻的時(shí)間點(diǎn)之間的可達(dá)關(guān)系與時(shí)間軸之間的可達(dá)關(guān)系是一致的,據(jù)定義1和2,可以將兩個(gè)框架合并。
　　定義3 他省且自省框架。一個(gè)他省且自省框架為一個(gè)三元組F=〈T,R?e,R?t〉。其中:T為時(shí)間點(diǎn)的集合;R?e為一個(gè)自反和傳遞的可達(dá)關(guān)系;R?t為一個(gè)傳遞可達(dá)關(guān)系。
　　其示意如圖1所示。
　　
　　直觀上T上的點(diǎn)通過R?t關(guān)系,構(gòu)成各條時(shí)間軸,每條時(shí)間軸代表一個(gè)主體(及其歷史數(shù)據(jù)庫),表示了自省關(guān)系;不同軸的同一時(shí)刻的時(shí)間點(diǎn)通過R?e,構(gòu)成了他省關(guān)系。

`NextPage`　　另一方面,作為他省關(guān)系,R?e為一個(gè)自反和傳遞的可達(dá)關(guān)系對(duì)于傳統(tǒng)BDI模型的認(rèn)知可達(dá)關(guān)系是一般的;而作為自省關(guān)系,R?t不能具有自反性。在直觀上,人的自省總是反省過去,對(duì)于現(xiàn)在是無法反省的,而作為他省關(guān)系的R?e的自反性,則主要體現(xiàn)了主體對(duì)自我知識(shí)集的認(rèn)知,因此需要保留。
　　在沒有具體解釋框架語義之前,針對(duì)R?e和R?t關(guān)系,分別用模態(tài)算子?□•和□對(duì)應(yīng)它們類似于經(jīng)典模態(tài)邏輯的必然關(guān)系,并由此用?□•□φ來表示一個(gè)主體有信念φ,假設(shè)這個(gè)主體是k,可以將其簡記為Bel(k)=?□•□φ。
　　2.2 Gentzen系統(tǒng)
　　據(jù)上,本文將對(duì)他省和自省框架構(gòu)造子結(jié)構(gòu)演算系統(tǒng),為體現(xiàn)子結(jié)構(gòu)演算特點(diǎn),在此用Gentzen風(fēng)格的演算系統(tǒng)(由德國人Gentzen 1934年在其博士畢業(yè)論文中提出的一種邏輯演算,國內(nèi)也翻譯為相繼式演算,但更多直譯為Gentzen演算,在該演算中分為結(jié)構(gòu)規(guī)則和運(yùn)算規(guī)則,運(yùn)算規(guī)則又分為左規(guī)則和右規(guī)則,是有別于Hilbert風(fēng)格的自然演繹方法的構(gòu)造性邏輯演算方法,主要用于證明論)來構(gòu)造BSoET,系統(tǒng)如下:
　　公