淺析智慧主體的信念認知時態子結構邏輯模型

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

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

　　a***主體理論模型中普遍存在邏輯全知***logic omniscience***。

　　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。由於BSoET系統採用的是子結構演算,有效避免了邏輯全知問題,其模型語義與構造性證明方法較經典二值邏輯更細精度地刻畫了信念的形成。

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