1、智能主体的信念认知时态子结构逻辑模型摘 要:智能主体获取信念的途径主要有两种:一种为他省,通过外界交互,从其他主体获取信息;另一种为自省,通过自己的历史数据库获取相关知识。对于主体信念的描述及刻画,两种途径缺一不可,但当前的 BDI理论模型中较多地为他省系统,没有做到两者相结合。其次,在当前的许多理论模型中,通常使用的是二值逻辑、经典模态逻辑或其变形系统,使得相应的逻辑系统普遍存在逻辑全知和粗精度刻画等问题。针对上述问题进行了探讨,采用了认知时态子结构逻辑建模的方法,表达了智能主体获得“双省”信念的方式,针对其建立了相应的逻辑系统 BSoET。 关键词:智能主体;信念;自省;他省;认知时态子结
2、构逻辑 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 approac
3、h 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
4、 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, thi
5、s 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 stat
6、e)。主体的心智状态为主体如何行动提供了一种解释,也就是说主体的行动是由主体的心智状态驱动的,如认知、情感、意向等。逻辑是描述主体心智状态的重要工具1。1990 年,Moore2使用形式逻辑对主体进行了建模,并主要研究了主体拥有的知识与实现的动作之间的关系;随后 Cohen 等人3系统地研究了信念、目标、持续目标、意图和理性的逻辑表达和演算问题,他们的工作基于线性时态逻辑,在语义上则以 Kripke 可能世界语义学为基础,并给出了 BDI 形式模型;其后,Rao 等人4提出了理想 agent 的 BDI 模型,使用了三个基本的模态算符:信念(belief)、愿望(desire)和意图(inte
7、ntion)建立了主体的BDI 模型;Jiao 等人5针对主体是在进程级运行的程序,运用 演算描述了主体的理性和行为意图,利用 演算这种刻画通信系统的进程演算表示出主体间的交互;胡山立等人6,7在真假子集语义基础上通过对模型的代数结构施加一定的约束,开发了双子集语义改进模型,避免了基于正规模态逻辑表示的逻辑全知问题以及由此带来的副作用等问题。此外,Konolige 等人813也做了相关值得肯定的工作,遍及 BDI 理论研究与应用的多个领域职称论文。 尽管 BDI 或类 BDI 模型已成为研究智能主体理论模型的主要工具,但这些模型仍普遍存在下述的一些问题: a)主体理论模型中普遍存在逻辑全知(l
8、ogic omniscience)1。 b)重视主体间知识交互,而轻视主体内部知识或状态。 c)由经典模态逻辑或二值逻辑引起的理论模型对真实世界的刻画粗精度。 基于此,本文针对上述问题进行了相关研究,并将研究工作聚焦于智能主体的信念,针对其作出了相关逻辑模型。考虑到对于愿望和意图,不同的应用和应用观对其有不同的看法和定义,因此本文并未进行深入研究,只着重刻画了认知和决策的关键,即信念。 1 智能主体信念的形成与表示 1.1 智能主体信念的形成及其问题 无论是 BDI 模型还是其他的智能主体的理论模型,对于信念的形成与表示都是建模的基础。但是在当前的许多理论模型中,对信念的形成存在一定的问题。例
9、如,作为经典的模型,在 Rao 等人4的模型中,在建模时虽使用到时态逻辑模型及其技巧,但仅考虑到系统的未来状态,而不关注过去的认知。实际上,造成类似的问题主要在于其对信念(知识)的获取仅考虑与外部主体进行交互,而轻视了主体在过去的知识。 事实上,作为一个智能主体,其获取信念(知识)的途径主要有两种:a)他省(extrospectiveness),即通过外界交互,从其他主体中获取信息;b)自省(introspectiveness),即通过自己的历史数据库获取相关知识的信息。因此,对于主体信念的描述与刻画,两种途径缺一不可。在当前研究中,体现他省的 BDI 模型较多,却较少带自省功能的模型。但从时
10、态数据库、时态知识库的角度看,智能主体的知识也是一个随着时间轴向前推进的历史数据库序列 H=(H?0,H?n,Hn+1,),在不同的阶段有不同的知识集,这些知识集对当前信念的建立影响巨大,自省不可忽视。因此,在逻辑建模中,必须体现他省和自省,并处理其间的各类知识冲突。 考虑到主体理论模型中普遍存在逻辑全知的问题,这也主要是因为相关模型使用了经典模态逻辑(或相关变形系统)、二值逻辑导致的结果。逻辑全知问题主要包括两个方面:a)一个主体如果知道一个命题,那么它知道它所知道的命题的全部逻辑后承。 b)一个主体知道所有的真理(重言式)。 造成问题 a)是因为理论模型采用了形如经典模态逻辑中的 K 公理
11、式的内定理。造成问题 b)的主要原因有两点:第一点是因为理论模型采用了形如经典模态逻辑中的 RN 规则式的规则造成;第二点是在计算科学,尤其是在机群协同工作下的智能主体的认知过程不应存在所谓的“重言式”模式的内定理,所有公式的成立与否都应采用构造性证明进行论证,而非传统的二值逻辑形式及其粗精度刻画。1.2 “双省”智能主体的信念表示 基于上述问题,本文提出了相应的解决方法。首先,主体的信念必须与他省和自省相结合。具体体现在不仅重视交互,而且重视历史数据。由此在表意上,可以使用 Bel(k)=KH 表示主体 k 在当前时刻具有信念 。其中:K 表示“知道”算子,体现了他省;H 仍使用时态逻辑中的
12、标记意义,表示“在此之前一直(不包括当前时间)”,体现了自省,只有当他省和自省都为“必然”时,知识才能成为信念。其次,要解决逻辑全知与非构造性语义的粗精度刻画问题,一种可行的方式是使用子结构逻辑(substructural logics)。根据子结构逻辑的构造性证明,能有效避免上述问题,并可通过结构规则的增删,修改传统 Hilbert 风格的逻辑演算所固留的诸如单调性、收缩性等弊病,以增加系统的可计算性。 据此,可建立相应的认知时态子结构逻辑系统。鉴于其表示了智能主体的信念,同时采用的是认知逻辑、时态逻辑和子结构演算的综合解决方法,本文将新的系统称为 BSoET 系统,意为 substruct
13、ural logic of epistemic and temporality in belief。在下一部分,将对系统作详细介绍。 2 BSoET 及其 Gentzen 系统 2.1 可能世界与可达关系 首先考虑到系统需要做到他省和自省,必须对认知的可能世界与可达关系作出定义,这种定义是针对框架的(frame)。 定义 1 他省框架。一个他省框架是一个二元组?F=T,R?e 。其中:T为时间结构的集合,对于每一个 T?iT,T?i 表示一个时间结构;R?e 为时间结构间的一个自反和传递的可达?关系。 直观上,对于每一个 T?iT,T?i 表示一个智能主体。这是考虑到每个智能主体都有一个历史数
14、据库,可以用 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 为一个传递
15、可达关系。 其示意如图 1 所示。 直观上 T 上的点通过 R?t 关系,构成各条时间轴,每条时间轴代表一个主体(及其历史数据库),表示了自省关系;不同轴的同一时刻的时间点通过 R?e,构成了他省关系。另一方面,作为他省关系,R?e 为一个自反和传递的可达关系对于传统 BDI 模型的认知可达关系是一般的;而作为自省关系,R?t 不能具有自反性。在直观上,人的自省总是反省过去,对于现在是无法反省的,而作为他省关系的 R?e 的自反性,则主要体现了主体对自我知识集的认知,因此需要保留。 在没有具体解释框架语义之前,针对 R?e 和 R?t 关系,分别用模态算子?和对应它们类似于经典模态逻辑的必然关
16、系,并由此用? 来表示一个主体有信念 ,假设这个主体是 k,可以将其简记为 Bel(k)=?。 2.2 Gentzen 系统 据上,本文将对他省和自省框架构造子结构演算系统,为体现子结构演算特点,在此用 Gentzen 风格的演算系统(由德国人 Gentzen 1934 年在其博士毕业论文中提出的一种逻辑演算,国内也翻译为相继式演算,但更多直译为 Gentzen 演算,在该演算中分为结构规则和运算规则,运算规则又分为左规则和右规则,是有别于 Hilbert 风格的自然演绎方法的构造性逻辑演算方法,主要用于证明论)来构造 BSoET,系统如下: 公理:A?A 结构规则: XAY,A,ZBY,X,
17、ZB(Cut) *XAXA(T for ?) *XA*XA(4 for ?) XAXA(4 for ) 运算规则: X,A,YCX,AB,YC(L) X,B,YCX,AB,YC(L) XA XBXAB(R) X,A,YC X,B,YCX,AB,YC(L) XAXAB(R) XBXAB(R) X,A,Y,B,ZCY,X,AB,ZC(L) X,ABXB(R) X,A,YBX,*?A,YB(?L) *XAX?A(?R)?X,A,YBX,A,YB(L) XAXA(R) 在此,“,” “*”“”分别是三个不同的 punc mark(句法标记,非算符)。其中“,”是一个无序的句法结构标记,它分割了多个参与
18、演算的公式序列;而“*”和“”分别是和的 punc mark14。其中结构规则“T for ”表明了如果公式序列 X 能在“*”的演绎下得到 A,则在一般演绎下也能得到 A,这恰好对应了 R?e 关系的自反性。类似地,结构规则“4 for ”对应了 R?e 关系的传递性,结构规则“4 for ”对应了 R?t 关系的传递性。 注意到,这是一个典型的“直觉主义”逻辑系统,是基于构造性证明的。同时由于类似 K 公理和 RN 规则的内定理不存在于 BSoET 的结构规则中,也有效避免了逻辑全知问题。值得一提的是,由于“L”规则的存在,系统实际保留了 Weakening 规则,即该系统的推理仍然是单调
19、的。同时由于punc mark“,”的无序性,交换律也依然保持其有效性,但系统不具有收缩规则,避免了运算资源的可重用性15。 另一方面,在 BSoET 系统中,本文也没有考虑算子“”,其主要原因是 BSoET 系统是一个直觉主义逻辑系统,其证明为构造性证明。由此,构造一个 的信念与构造一个 的信念的工作是相似的。 3 BSoET 系统的语义模型 定义 4 点集与命题14。一个点集 P=P,为集合 P 及其上的偏序关系。P 上的命题集 Prop(T)为 P 上的所有向上封闭的子集 X,即若 xX且 xx,则 xX。定义 5 可达关系。 1)二元关系 R 为点集 P 上的二元关系当且仅当对?x,y
20、P,如果 xSy且?x(xx),则?y(yy),使得 xRy。类似地,如果 xRy 且?y(yy),则?x(xx),使得 xRy。 2)二元关系 R 为点集 P 上的丰满的(plump)二元关系,当且仅当对于?x, y, x, yP,如果 xRy 且 xx,yy,则 xRy。定义 6 框架及框架关系。一个框架 F 为一点集 P 及其上的二元可达关系,写做 F=P,R?e,R?t 。其中 R?e 和 R?t 分别为他省和自省的二元关系。 定义 7 框架赋值。 1)xF:x?pPropF; 2)x?AB iff ?xF, x?A 且 x?B; 3)x?AB iff ?xF, x?A 或 x?B; 4)x?A iff ?yF,如果 x R?e y,则 y?A; 5)x?A iff ?yF,如果 x R?t y,则 y?A。 定义 8 衍推。 1)称 X 相对于模型 M 衍推 A,记做“X?MA”,当且仅当对?xM,如果x?X,则 x?A; 2)称 X 相对于框架 F 衍推 A,记做“X?FA”,当且仅当对?MF,X?MA; 3)称 X 相对于框架类 F 衍推 A,记做“X?F A”,当且仅当对?FF,X?FA。 由此易证得以下定理,限于篇幅证明从略,有兴趣的读者可以参见文献16。
