体现了主体对自我知识集的认知，因此需要保留。
　　在没有具体解释框架语义之前，针对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模型，并最后付诸领域应用。
　　

参考文献

　　[1]史忠植.智能主体及其应用[M].北京:科学出版社，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].软件学报，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]刘冬宁.时态信息处理中若干问题的逻辑公理化研究[R].广州:中山大学，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.