智能主体的信念认知时态子结构逻辑模型

　　现在大学及以上学历毕业时要想获得学位证必须写一篇毕业论文并通过论文答辩。然而，写一篇优秀的毕业论文非常有难度。下面文书帮小编就为大家带来一篇优秀的计算机毕业论文，供大家阅读参考!

       摘 要:智能主体获取信念的途径主要有两种:一种为他省,通过外界交互,从其他主体获取信息;另一种为自省,通过自己的历史数据库获取相关知识。对于主体信念的描述及刻画,两种途径缺一不可,但当前的BDI理论模型中较多地为他省系统,没有做到两者相结合。其次,在当前的许多理论模型中,通常使用的是二值逻辑、经典模态逻辑或其变形系统,使得相应的逻辑系统普遍存在逻辑全知和粗精度刻画等问题。针对上述问题进行了探讨,采用了认知时态子结构逻辑建模的方法,表达了智能主体获得“双省”信念的方式,针对其建立了相应的逻辑系统BSoET。

　　关键词:智能主体;信念;自省;他省;认知时态子结构逻辑

　　引言

　　为适应环境变化和协作求解,智能主体(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关系的传递性。