智能主体的信念认知时态子结构逻辑模型
若水分享
1147
摘 要:智能主体获取信念的途径主要有两种:一种为他省,通过外界交互,从其他主体获取信息;另一种为自省,通过自己的历史数据库获取相关知识。对于主体信念的描述及刻画,两种途径缺一不可,但当前的BDI理论模型中较多地为他省系统,没有做到两者相结合。其次,在当前的许多理论模型中,通常使用的是二值逻辑、经典模态逻辑或其变形系统,使得相应的逻辑系统普遍存在逻辑全知和粗精度刻画等问题。针对上述问题进行了探讨,采用了认知时态子结构逻辑建模的方法,表达了智能主体获得“双省”信念的方式,针对其建立了相应的逻辑系统BSoET。
关键词:智能主体;信念;自省;他省;认知时态子结构逻辑
Substructural logic of epistemic and temporality in belief of agent
LIU Dong-ning?1,TANG Yong?2
(1.School of Computer, Guangdong University of Technology, Guangzhou 510006, China;2.School of Computer, South China Normal University, Guangzhou 510631, China)
Abstract:There are two kinds of approach to get belief as an agent. One is extrospectiveness, which gets information from other body through outside interaction. The other is introspectiveness, which gets information from own history database. The two ways are indispensable to describe belief of agent. However, nowadays BDI logics mostly use extrospectiveness, not combination of extrospectiveness and introspectiveness. Also, most BDI logics are usually based two-value logic, classical modal logic or its transmutation, which makes many logic systems have problems such as logic omniscience and coarse depiction.For these problems, this paper made some research and put forward a substructural logic of epistemic and temporality(BSoET)focusing as belief of agent.
Key words:agent; belief; introspectiveness; extrospectiveness; substructural logic of epistemic and temporality
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。由于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.
关键词:智能主体;信念;自省;他省;认知时态子结构逻辑
Substructural logic of epistemic and temporality in belief of agent
LIU Dong-ning?1,TANG Yong?2
(1.School of Computer, Guangdong University of Technology, Guangzhou 510006, China;2.School of Computer, South China Normal University, Guangzhou 510631, China)
Abstract:There are two kinds of approach to get belief as an agent. One is extrospectiveness, which gets information from other body through outside interaction. The other is introspectiveness, which gets information from own history database. The two ways are indispensable to describe belief of agent. However, nowadays BDI logics mostly use extrospectiveness, not combination of extrospectiveness and introspectiveness. Also, most BDI logics are usually based two-value logic, classical modal logic or its transmutation, which makes many logic systems have problems such as logic omniscience and coarse depiction.For these problems, this paper made some research and put forward a substructural logic of epistemic and temporality(BSoET)focusing as belief of agent.
Key words:agent; belief; introspectiveness; extrospectiveness; substructural logic of epistemic and temporality
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。由于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.