林 穎，衛(wèi) 龍

(1.寧德師范學院馬克思主義學院，福建 寧德 352100；2.安徽大學哲學學院，安徽 合肥 230039）

Agent（主體）是人類智能、動物智能和機器智能的統(tǒng)一模型[1]3。理性Agent具有知識、信念、愿望、意圖和行為，如何對這些概念及其相互關(guān)系進行形式化是分析哲學、邏輯學和人工智能長期關(guān)注的課題。如何形式化地表征“動態(tài)信念和知識對單主體行為的影響”，國內(nèi)外不乏這方面的邏輯模型。在多主體環(huán)境下，如何形式化地描述動態(tài)信念和知識對多主體行為的影響呢？本文構(gòu)建的關(guān)于動態(tài)信念和知識的多主體邏輯（簡記為BDL邏輯），試圖回答這一問題。

一、引言

在20世紀，關(guān)于Agent研究主要集中在兩個方面：一是知識和信念等信息方面；二是承諾和義務(wù)等動機方面。后來的發(fā)展主要包括：面向主體的編程、對理性主體進行形式化的BDI結(jié)構(gòu)、對多主體系統(tǒng)進行形式說明和驗證的邏輯、受限理性主體邏輯和認知機器人學、對理性主體（各個方面的）行動進行說明和推理的邏輯。以上這些主要研究了主體的信息和行動特征，而忽略了主體動機方面的特征。在隨后的研究中，用以下內(nèi)容對這些邏輯框架進行了擴展，包括：不確定性行動、認知測試和交際行動、模擬缺省推理行動[2]。執(zhí)行行動的結(jié)果可以被定義為“行動的執(zhí)行所導致的事件狀態(tài)”[3]。

多位學者使用不同的方法研究了面向Agent的系統(tǒng)。在對主體和多主體系統(tǒng)進行研究和形式化時，經(jīng)常用到邏輯方法，尤其是模態(tài)邏輯。在所有主體系統(tǒng)中，較為著名的具有模態(tài)特征的主體形式系統(tǒng)有：動態(tài)邏輯和認知邏輯的融合系統(tǒng)[4]、BDI系統(tǒng)[5]、KARO框架[6]、知識和信念的時態(tài)邏輯[7]、關(guān)于信念和更新的模態(tài)邏輯框架[8]、動態(tài)認知邏輯[9]。

在這些系統(tǒng)中，最為著名且應(yīng)用最廣的是BDI系統(tǒng)。BDI系統(tǒng)[5]認為：Agent是具有信念、愿望和意圖（Belief-Desire-Intention，簡稱BDI）這三種心智態(tài)度的理性主體；信念是主體系統(tǒng)的信息內(nèi)容；愿望是主體系統(tǒng)的動機狀態(tài)；意圖是主體系統(tǒng)的慎思內(nèi)容。因此，BDI表征了主體的信息、動機和慎思狀態(tài)。當慎思（deliberation）受制于資源時，這些心智態(tài)度決定了主體系統(tǒng)的行為，因而是達成適當或最優(yōu)性能的關(guān)鍵[10]。主體行為可以看成是“由系統(tǒng)直接執(zhí)行的時態(tài)邏輯說明”[11]。IRMA系統(tǒng)[12]和PRS-類系統(tǒng)[13]，都是對理性主體的BDI邏輯系統(tǒng)的不同實現(xiàn)。

BDI邏輯能夠描述信念和知識對主體行為的影響，而BDI邏輯的基礎(chǔ)系統(tǒng)是命題動態(tài)邏輯PDL（簡稱PDL）[14]。PDL邏輯有兩種語言：程序語言和命題語言，能夠?qū)Τ绦蚧蛐袆舆M行推理。模態(tài)邏輯系統(tǒng)S5[15]能夠?qū)χR進行推理，公式□φ可以解讀為“主體知道φ”。因此，對PDL中測試算子的語義和形式系統(tǒng)進行重新描述，并采用“能夠?qū)Τ橄笮袆雍途唧w行動加以區(qū)分的”新的行為表示方法，就可以達到對多主體環(huán)境下的動態(tài)信念和知識建模的目的。這種新的測試算子被稱為信息測試算子，可以用來把特定主體的信念和知識形式化為動態(tài)模態(tài)詞。這種信息測試算子與K(D)45和S5這類系統(tǒng)中的“能夠?qū)χ黧w的信念和知識進行形式化的模態(tài)詞”類似。這種把PDL和S5進行融合后得到的邏輯就是本文重點研究的動態(tài)信念和知識的多主體邏輯（簡稱BDL），該邏輯是BDI邏輯的變種。

在哈瑞（Harel）等[14]、布拉克布恩（Blackburn）等[15]、斯密迪特（Schmidt）[16]和提西孔思科（Tish‐kovsky）[17]、張曉君[1]等文獻的基礎(chǔ)上，本文試圖形式化地描述動態(tài)信念和知識與多主體行為之間的關(guān)系。其基本思路是：通過引入信念或者知識的確認行動，把主體的隱性信息態(tài)度（信念或者知識）進行顯性化。信念（或者知識）確認行動是通過改進后的測試算子（即信息測試算子）進行建模。信息測試算子只具有確認信念或者知識狀態(tài)中的公式的能力，不具有很強的確認當前世界所有真實性質(zhì)的能力。

BDL邏輯語言具有較強的表達力，這種表達力主要是通過向主體信念中引入動態(tài)性來實現(xiàn)的，即把新的信息測試算子整合進主體信念中。雖然信息測試算子具有許多優(yōu)點，但是對抽象行動和具體行動進行區(qū)分也是至關(guān)重要的，有了這種區(qū)分才能夠?qū)Χ嘀黧w間的合作與團隊協(xié)同進行推理，而不僅僅是對單主體的推理[18]。

二、BDL邏輯的語言和語義

由于主體行為具有不可預(yù)測性，即必須反映系統(tǒng)的不確定性，這就要求其形式語義學是狀態(tài)語義學。此外，要求主體具有智能，可以把簡單的行動組合成復(fù)雜的行動。允許任意主體執(zhí)行的行動稱為抽象行動；抽象行動可以是原子行動也可以是復(fù)合行動。抽象行動只是主體可以執(zhí)行的真實而具體的行動的名稱。任何具體的行動總是與某個主體相關(guān)聯(lián)，因為不同的主體可以以不同的方式執(zhí)行（抽象）行動。

假設(shè)主體希望自己可以選擇如何執(zhí)行一個行動，這也是非確定性行動或者執(zhí)行替代路徑的動機。非確定性實際上意味著主體沒有關(guān)于系統(tǒng)行為的完整信息，或者很難獲取或者存儲此類信息。此外，即使與不同的主體相關(guān)聯(lián)的具體行動也可以由復(fù)雜的行動組成，這一性質(zhì)對于描述多主體的團隊協(xié)作非常有利。

由于主體具有智能，它們必須對世界有一些了解，或者至少有一些信念或者知識?？梢园阎黧w的信念（或者知識）看作是主體相信（或者知道）的公式集。因為主體在其活動中執(zhí)行行動和“學習”，所以在信念（或知識）與行動之間必須有某種相互依存的關(guān)系。獲得關(guān)于主體信念或者知識的信息，其實是主體頭腦中的某種行動。主體的信念和知識通過動態(tài)信息測試算子進行整合，該算子確認主體的信念（或知識），而不是像命題動態(tài)邏輯PDL中的經(jīng)典測試算子那樣確認實際狀態(tài)的性質(zhì)。

（一）BBDDLL邏輯的語言

BDL邏輯語言由四種不相交的成分組成：主體集?、抽象行動集Π1、具體行動集Π2和公式集Σ。抽象行動可以是原子行動，也可以是復(fù)合行動。具體行動是“具體主體執(zhí)行的”抽象行動，它們也可組合成復(fù)雜的具體行動，這些行動的語義必須包含主體的非確定性。通常，用公式描述多主體系統(tǒng)的性質(zhì)。

使用如下集合和邏輯聯(lián)結(jié)詞可定義BDL邏輯的語言L：命題變元的可數(shù)集Δ={p，q，r，…}、抽象原子行動變元的可數(shù)集Π0={a，b，c…}，以及主體變元的可數(shù)集?={i，j，k，…}。邏輯聯(lián)結(jié)詞包括經(jīng)典聯(lián)結(jié)詞，→和⊥，信息測試算子，行動公式的標準命題動態(tài)邏輯PDL的聯(lián)結(jié)詞∪（程序不確定性選擇算子）、；（程序的序列合成算子）和*（程序迭代算子），以及動態(tài)模態(tài)算子[]（box算子）。抽象行動、具體行動和公式可以同時使用歸納的方式加以定義，使得抽象行動集Π1、具體行動集Π2和公式集Σ是滿足以下條件的最小集合。 ∩

（1）Π0? Π1，Δ{⊥}? Σ；

（2）如果φ?Σ并且α，β?Π1，那么φ，α*，α∪β，α；β?Π1

（3）如果α?Π1并且i??那么αi?Π2；

（4）如果α，β?Π2那么α*，α∪β，α；β?Π2；

（5）如果φ，ψ?Σ并且α?Π2那么φ→ψ，[α]φ?Σ。

﹁，?，^，ˇ，?這些公式聯(lián)結(jié)詞可以用通常的方式由經(jīng)典聯(lián)結(jié)詞→和⊥加以定義。diamond算子〈〉是box算子[]的對偶，即〈α〉φ?﹁[α]﹁φ。信念算子Bi定義為模態(tài)算子(??)i。公式Bip讀作“主體i相信p”。

公式集Σ的任意子集在分離規(guī)則、概括規(guī)則和替換規(guī)則下封閉。

分離規(guī)則：如果φ且φ→ψ成立，那么ψ成立，即φ，φ→ψ?ψ。

概括規(guī)則：如果φ成立，那么[α]φ成立，即φ?[α]φ。

其中φ，ψ?Σ并且α?Π2。

注記：（1）如果變元x在φ中的所有出現(xiàn)都被ψ中的項s替換，那么公式ψ是用s替換x時φ的替換實例，記作ψ=φ{(diào)s/x}。（2）令a是原子抽象行動，j是具體行動α中的主體變元，那么在a替換aj的情況下，公式ψ是φ的替換實例，記作ψ=φ{(diào)α/aj}。（3）對于任意兩個公式集Γ和Λ，Γ⊕Λ表示同時包含Γ和Λ的最小邏輯；具體地說，PDL和S5融合后的邏輯記作：PDL⊕S5。

（二）BBDDLL邏輯的語義

BDL模型是四元組M=〈S，f，g，?〉的克里普克模型，使得M1=〈S，f，?〉是PDL模型，M2=〈S，g，?〉是S5模型；其中S是一個非空的狀態(tài)集，f是把每個具體行動a與一個二元關(guān)系f(a)關(guān)聯(lián)起來的映射，g是從主體集合到S上的傳遞關(guān)系和歐幾里得關(guān)系集的映射，?是克里普克模型上的真值關(guān)系。任何BDL模型都必須滿足以下10個條件。對于任何具體行動α和β，映射f應(yīng)該滿足的一般條件是：

(M1)：f(α∪β)=f(α)∪f(β)

(M2)：f(α；β)=f(α)°f(β)

(M3)：f((α)*)=(f(α))*

這里“°”表示關(guān)系組合，*是關(guān)系上的自返傳遞閉包算子。對于任何抽象行動α、β和主體i，把具體行動與抽象行動聯(lián)系起來的映射f應(yīng)該滿足的條件是：

(M4)：f((α∪β)i)=f(αi∪βi)

(M5)：f((α；β))i=f(αi；βi)

(M6)：f((α*)i)=(f(αi))*

關(guān)于真值關(guān)系的標準條件必須為真，其中s表示任意狀態(tài)，ψ和φ是任意公式，α是任意具體行動：

(M7)：M，s?⊥

(M8)：M，s?φ→ψ ? M，s?φ ? M，s?ψ

(M9)：M，s?[α]φ ? ?t((s，t)?f(α)? M，s?φ)

信息測試算子的語義為：

公式φ在模型M的狀態(tài)s中有效，記作M，s?φ；如果φ在模型的所有狀態(tài)下都有效，那么就說φ在模型M中是有效的。BDL邏輯是在所有BDL模型中有效的公式集。

三、BDL邏輯的公理化、可判定性和復(fù)雜性

通過如下公理、分離規(guī)則、概括規(guī)則和替換規(guī)則，可以給出BDL邏輯的希爾伯特式公理化系統(tǒng)。BDL邏輯包含如下公理：

(A1)經(jīng)典命題邏輯的公理

(A2)無測試行動的命題動態(tài)邏輯PDL的類似公理：

(A2.3)[ai；bj]p?[ai][bj]p

(A2.4)[(ai)*]p→p^[ai]p

(A2.5)[(ai)*]p→[ai][(ai)*]p

(A2.6)p^[(ai)*](p→ [ai]p)→ [(ai)*]p

(A3)信念算子的K45公理：

(A3.1)Bip→BiBip

(A3.2) ﹁Bip→ Bi﹁Bip

(A4)抽象行動與具體行動之間的對應(yīng)公理：

(A4.2)[(a；b)i]p?[ai；bi]p

(A4.3)[(a*)i]p?[(ai)*]p

(A5)信息測試算子公理：

由于BDL邏輯是由命題動態(tài)邏輯PDL和模態(tài)邏輯S5融合而成，融合邏輯系統(tǒng)可以繼承其組成邏輯的諸多優(yōu)良性質(zhì)，如可靠性、完全性、有窮模型性質(zhì)和可判定性[19][20]。由于PDL和S5都具有這四個性質(zhì)，因此BDL邏輯也具有這四個性質(zhì)。利用模態(tài)邏輯和動態(tài)邏輯方法，可以給出BDL邏輯這四個性質(zhì)的證明；但是由于新的信息測試算子的存在，只需對其證明進行必要的修改即可，因此本文只給出其結(jié)論，并不給出這四個性質(zhì)的詳細證明。

定理 11（完全性）：上述BDL公理系統(tǒng)對于所有BDL模型類是完全的。

現(xiàn)在討論BDL邏輯的有用擴展。在一些多主體系統(tǒng)中的一些主體比BDL邏輯中的主體具有更高的智能。通常要求主體的信念能夠充分反映系統(tǒng)的性質(zhì)，這時，主體的信念實際上變成了知識。為了使主體具有這種額外智能，需要在BDL邏輯中添加T公理：Bip→p，這時的BDL邏輯中信念算子Bi就是S5系統(tǒng)中的模態(tài)詞，代表知識算子。此外，還要求主體信念具有一致性，該性質(zhì)可以通過在BDL邏輯中添加D公理來表示：Bip→﹁Bi﹁p。

在對智能主體進行建模時，一個關(guān)鍵問題就是弄清信息態(tài)度和行動之間的聯(lián)系。信息態(tài)度和行動之間最廣為人知和最自然的聯(lián)系是無學習和完美回憶（perfect recall）[21]。無學習性質(zhì)通常由NL公理模式來表示：[ai]Bip→Bi[ai]p，其中Bi通常表示認知算子；其意思是：主體i事先知道其行動的結(jié)果，即：不需要學習。完美回憶通常由公理模式PR來表示：Bi[ai]p→[ai]Bip；它表示在執(zhí)行一個行動之后，主體的知識（有時是信念）具有持久性。

還可以要求這些模型具有如下性質(zhì)：

等價性：?igi是一個等價關(guān)系

持續(xù)性：?i?s?t(s，t)?gi

左交換性：?i?α(gi°f(αi)?f(αi)°gi)

右交換性：?i?α(f(αi)°gi?gi°f(αi)

定理 22（完全性）：令L是由公理T、D、NL和PR的任意組合而形成的BDL邏輯的擴展系統(tǒng)，那么L相對于“具有等價性、持續(xù)性、左交換性和右交換性的相應(yīng)組合的”所有模型類而言，都是完全的。

定理 44（可判定性和復(fù)雜性）：由公理T、D、NL和PR的所有可能組合構(gòu)成的BDL邏輯的所有擴張邏輯的可滿足性問題，以及BDL邏輯本身的可滿足性問題，在EXPTIME（確定性指數(shù)時間）中是很難判定的，但是在2EXPTIME（即2倍確定性指數(shù)時間）內(nèi)是可以判定的。

現(xiàn)在在BDL⊕T中定義（完全測試）命題動態(tài)邏輯PDL的一個翻譯。選擇一個主體，比如主體i，然后定義從PDL公式到公式集Σ的映射h如下：

下面的定理表明，翻譯函數(shù)h在兩個方向上都保持了公式的真值。

定理 55：對于任意命題動態(tài)邏輯PDL公式φ，φ?PDL，當且僅當，h(φ)? BDL⊕ T。

施歸納于公式集Σ中公式的結(jié)構(gòu)，即可證明定理5。或者參照張曉君（2017）[1]102-103中的等級BDI邏輯到PDL的翻譯函數(shù)的類似證明亦可得證。

沒有（經(jīng)典）測試算子的命題動態(tài)邏輯PDL是BDL邏輯的一個子邏輯。因此，BDL邏輯可以對BDL邏輯中的簡單程序（如while程序）進行推理。為了能夠?qū)θ魏纬绦蜻M行推理，定理5對BDL邏輯進行了最小強化。

信息測試行動最重要的特征是：可以使主體的內(nèi)隱信念得到顯性化。確認公式的行動和確認公式的否定的行動都可以為主體提供信念（知識），這種組合行動是一種信息行動[23]。任何確認公式及其否定公式的行動都是“二選一測試”（alternative test）[24]。該測試的特點是：被測公式的真假不應(yīng)受到實際測試行為的影響，即測試的結(jié)果應(yīng)與被執(zhí)行的測試的狀態(tài)相對應(yīng)，這一特性稱為真實性（truthfulness）

“二選一測試”具有最小更新性質(zhì)，其意思是：這種測試不能從“與測試行為無關(guān)的主體的信念集中”添加或者刪除公式。這意味著，如果一個主體在下載文件之前認為“北京是中國的首都”，那么在文件下載后她仍然會認為“北京是中國的首都”。

四、結(jié)束語

本文的研究表明：（1）把模態(tài)邏輯S5系統(tǒng)與命題動態(tài)邏輯PDL進行融合，并對PDL邏輯中的測試算子的語義和形式系統(tǒng)進行重新描述，可以得到動態(tài)信念和知識的多主體邏輯BDL；這種新的信息測試算子能夠使得主體的動態(tài)信息（如知識）、這些動態(tài)信息的真實性和信念得以保持；（2）BDL邏輯是信念-愿望-意圖邏輯BDI（其基礎(chǔ)系統(tǒng)是PDL邏輯）的變種，采用“能夠?qū)Τ橄笮袆雍途唧w行動加以區(qū)分的”新的行為表示方法，可以達到對多主體環(huán)境下的動態(tài)信念和知識建模的目的；（3）BDL邏輯不僅可以表達共同的信念和共同的知識，而且這種帶有信念和知識模態(tài)詞的多主體邏輯比PDL邏輯具有更強的表達力；（4）BDL邏輯的復(fù)雜性在2EXPTIME（即2倍確定性指數(shù)時間）之內(nèi)；（5）BDL邏輯不僅可以表征多主體環(huán)境下信念或者知識的自然屬性，而且還可以表征信念或者知識與行動之間的交互。

未來的工作可以考慮：如何在BDL邏輯框架中，對“能夠?qū)χR進行推理的”其他邏輯進行適當?shù)墓砘窟@些邏輯的可判定性如何？