本文針對智能主體的“雙省”信念及其形成與表示進行了相關研究,采用了認知時態子結構邏輯建模的方法,表達了智能主體獲得“雙省”信念的方式,針對其建立了相應的邏輯系統BSoET。由于BSoET系統采用的是子結構演算,有效避免了邏輯全知問題,其模型語義與構造性證明方法較經典二值邏輯更細精度地刻畫了信念的形成。

　　《電子設計應用》國家級電子技術期刊，堅持為社會主義服務的方向，堅持以馬克思列寧主義、毛澤東思想和鄧小平理論為指導，貫徹“百花齊放、百家爭鳴”和“古為今用、洋為中用”的方針，堅持實事求是、理論與實際相結合的嚴謹學風，傳播先進的科學文化知識，弘揚民族優秀科學文化，促進國際科學文化交流，探索防災科技教育、教學及管理諸方面的規律，活躍教學與科研的學術風氣，為教學與科研服務。

　　0 引言

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

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

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

　　b)重視主體間知識交互,而輕視主體內部知識或狀態。

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

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

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

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

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

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

　　考慮到主體理論模型中普遍存在邏輯全知的問題,這也主要是因為相關模型使用了經典模態邏輯(或相關變形系統)、二值邏輯導致的結果。邏輯全知問題主要包括兩個方面:

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

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

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

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

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

　　據此,可建立相應的認知時態子結構邏輯系統。鑒于其表示了智能主體的信念,同時采用的是認知邏輯、時態邏輯和子結構演算的綜合解決方法,本文將新的系統稱為BSoET系統,意為substructural logic of epistemic and temporality in belief。在下一部分,將對系統作詳細介紹。

　　2 BSoET及其Gentzen系統

　　2.1 可能世界與可達關系

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

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

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

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

　　假定不同軸的同一時刻的時間點之間的可達關系與時間軸之間的可達關系是一致的,據定義1和2,可以將兩個框架合并。

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

　　其示意如圖1所示。

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

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

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

　　2.2 Gentzen系統

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

　　公理:A?A

　　結構規則:

　　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 □)

　　運算規則:

　　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(句法標記,非算符)。其中“,”是一個無序的句法結構標記,它分割了多個參與演算的公式序列;而“*”和“○”分別是□•和□的punc mark[14]。其中結構規則“T for □•”表明了如果公式序列X能在“*”的演繹下得到A,則在一般演繹下也能得到A,這恰好對應了R?e關系的自反性。類似地,結構規則“4 for □•”對應了R?e關系的傳遞性,結構規則“4 for □”對應了R?t關系的傳遞性。

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

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

　　3 BSoET系統的語義模型

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

　　定義5 可達關系。

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

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

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

　　定義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”,當且僅當對?x∈M,如果x?X,則x?A;

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

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

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

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

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

　　4 群體信念與公共信念

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

　　基于BSoET系統,易得在群體認知中的群體信念“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 結束語

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