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模型,并最后付诸领域应用。
参考文献:
[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.
