时态逻辑及其在决策系统中的应用精品文稿.ppt

《时态逻辑及其在决策系统中的应用精品文稿.ppt》由会员分享，可在线阅读，更多相关《时态逻辑及其在决策系统中的应用精品文稿.ppt（25页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、时态逻辑及其在决策系统中的应用第1页，本讲稿共25页 断言推理1目目录 时态逻辑 2 SIDSS系统描述 3 系统实现4 总结 5第2页，本讲稿共25页 断言推理1PrePost由这样的断言推理为核心组织的产生式系统在决策支持系统、专家系统中使用得最多，也是最为成熟的解决方案但是语义是静态的当遇到诸如动态的、实时的、并发的或具有其他时态特性的推理时，这种静态的推理方式则有很大的缺陷时态逻辑断言推理则可有效地弥补这方面出现的难题。第3页，本讲稿共25页 时态逻辑2时态逻辑（tense logic）是非经典逻辑的分支学科其研究对象是:把含有时态动词的语句形式化 把含有这种语句的推理系统化引入以下常

2、见的时态逻辑操作符：Next:A,If A and B are formulae thenAAlways:A,Always in the future ASometimes:A,Sometimes in the future AUntil:AUB,A until BSince:ASB,A since BAfter:AB,B after A第4页，本讲稿共25页 系统描述3智能工资决策支持系统（SIDSS）是由刘冬宁、汤庸等人自主开发的一个典型的时态信息系统目前已有6000多家机关事业单位用户针对我国机关事业单位工资政策复杂性、地域性和时间性等主要特点应用时态数据和知识处理技术解决了根据机关事业

3、单位工作人员随时间变化影响工资变动的信息（时态性数据），依据相应时期的工资政策（时态知识库）自动确定工资的问题第5页，本讲稿共25页3.1 SIDSS中的时态特征根据我国国情，工资政策繁杂，随时间变动大在复杂的规则、高时态信息变动的条件下如何确保工资确定的正确性成了SIDSS中的重点和难点涉及到了大量的断言推理与时态信息处理 系统描述3第6页，本讲稿共25页简单地以工资政策中“两年优秀晋升”的政策为例该政策在1999年以前的描述是这样的：如果人员连续两年考核优秀，或某年考核优秀有“一年优”标志，工资档次允许晋升一档，考核结果有效年份从下年算起，但连续两次晋升之间必须相隔两年以上。在1999年以

4、后的描述则改为：其他与之前相同，但连续两次晋升之间必须相隔四年以上。举例说明：人员A从1995年到2000年的考核均为优秀，则他可以分别在1997年和1999年执行一次工资档次晋升，而不允许在2001年执行档次晋升，正是由于1999年以后的工资政策规定，2001年与1999年之间并未相隔4年以上，因此不能进行晋升 系统描述3第7页，本讲稿共25页表1人员A工资晋升随时间的变化年份年份考核结果考核结果执行操作执行操作政策依据政策依据1995优秀 1999年以前的“两年优晋升”相隔必须两年以上1996优秀1997年允许晋升一档1997优秀 1998优秀1999年允许晋升一档1999优秀 1999年

5、以后的“两年优晋升”相隔必须四年以上2000优秀2001年不允许晋升一档 系统描述3第8页，本讲稿共25页3.2 规则描述在“人员越级晋升”的过程中，会遇到的各种规则本文中仅以1999年更改政策一项规则变更为基准其规则、条件、动作的相关表如下：系统描述3第9页，本讲稿共25页规则规则规则名规则名规则说明规则说明起始条件表达式起始条件表达式规则生命周期规则生命周期R1越级晋升用于处理1999年以前考核结果引起的越级晋升C11993/10,1998/12R2越级晋升用于处理1999年以后考核结果引起的越级晋升C21999/1,NOW表2 越级晋升规则表 系统描述3第10页，本讲稿共25页表3 越级

6、晋升条件表条件条件条件条件THENELSEC1连续两年考核结果优秀C3NULLC2连续两年考核结果优秀C4NULLC3当前年份上次越级晋升年份=2 或以前从未越级晋升A1NULLC4当前年份上次越级晋升年份=4 或以前从未越级晋升A1NULL 系统描述3第11页，本讲稿共25页表4 越级晋升动作表动作动作动作动作NEXTA1人员工资档次加一档NULL表24中，是关于“越级晋升”这一事件涉及到的规则、条件和动作。从表中可以看到这样的规则、条件、动作具有断言推理的特征，而其中在规则表中，定义的生命周期，更体现了时态变更性的特点，同时这一系列的判断推理都具有强时序性，鉴于对推理的正确性应引入时态逻辑

7、断言推理。系统描述3第12页，本讲稿共25页4.1 时态逻辑断言规则的设计根据表24，设计执行规则如下：（S1）When ReceivePromotingApplicationThen_Do TimeVerification And_Then CondictionChecking（S2）When CondictionCheckingThen_Do PromotionExecuting在执行规则中体现出了较强的时间序列性（1）接到越级晋升的请求后，先判断系统时间，根据规则的生命周期挑出该使用的条件序列判断；（2）完成匹配条件序列判断嵌套；（3）执行动作。系统实现4第13页，本讲稿共25页进一步细

8、化这些执行序列：（S3）When CondictionCheckingIf InvalidCondictionThen_Do Next_CondictionChecking Until EndofLayer_CondictionChecking在条件判断嵌套过程中，当前条件得不到匹配时，则轮转到下一条件进行匹配，直到该层所有条件判断完毕即判断嵌套完成 系统实现4第14页，本讲稿共25页（S4）When CondictionCheckingIf EndofLayer_CondictionCheckingThen_Do RejectPromotingApplication在条件判断嵌套过程中，当前

9、条件得不到匹配和该层所有条件又判断完毕时，则表示不符合越级晋升的条件，不通过该处理（S5）WhenNot InvalidCondictionThen_Do NextLayer_CondictionChecking Until EndofAll_CondictionChecking And_Then PromotionExecute在条件判断嵌套中，当前条件匹配成功则递进到下一层条件判断，如所有条件没有判断完毕则继续进行判断嵌套直到嵌套完毕，如嵌套完毕而条件匹配又成功则执行晋升动作 系统实现4第15页，本讲稿共25页4.2 对断言规则的逻辑描述对（S1）、（S2）逻辑描述如下：（S6）recei

10、ve(SIDSS,Promoting_Application)=verify(SIDSS,System_Time)check(SIDSS,Condiction)其中“”表示After，AB，意为B after A。（S7）check(SIDSS,Condiction)=act(SIDSS,Promotion)系统实现4第16页，本讲稿共25页对（S3）-（S5）逻辑描述如下：（S8）check(SIDSS,Condiction)match(SIDSS,Condiction)=samelayer_check(SIDSS,Condiction)U end_check(Condiction,Laye

11、r)其中“U”在这里代表Until。（S9）match(SIDSS,Condiction)end_check(Condiction,Layer)=reject(SIDSS,Promoting_Application)（S10）match(SIDSS,Condiction)=(nextlayer_check(SIDSS,Condiction)U end_check(Condiction,All)act(SIDSS,Promotion)系统实现4第17页，本讲稿共25页4.3 对规则生命周期的时态逻辑表示不仅可以对推理规则进行时态逻辑断言设计以及逻辑推理，还可对规则的生命周期也用时态逻辑进行扩展。

12、引入时态因子Ti时态因子时态因子状态状态T1表示时间T2表示时间表5 时态因子表 系统实现4第18页，本讲稿共25页因此对规则R1和R2的表示分别为：（1）Always R1 Since T1 Until T2（2）Always R2 Since T2用时态逻辑运算符表示为：（1）(R1 S T1)U T2)（2）(R2 S T1)系统实现4第19页，本讲稿共25页4.4 Java实现根据上述时态逻辑断言，可以在代码中实现上述规则断言。调用Time Rover Inc.的Temporal Rover工具它是一种用于处理Java程序中时态逻辑断言并根据断言生成有效Java代码的工具，并可以配备数

13、据库表的工具DBRover同时使用。系统实现4第20页，本讲稿共25页给出断言规则（S6）-（S7）的Java伪代码如下所示：S6:receive Promoting_Application implies Next checkCondiction Until verify SystemTime;S7:Always match Condiction implies Next act Promotion;系统实现4第21页，本讲稿共25页给出断言规则（S8）（S10）的Java伪代码如下所示：S8:If!match Condiction implies Nextcheck Next_Condic

14、tion Until EmptyCondiction of this Layer;S9:If EmptyCondiction of this Layer implies Next!act Promotion;S10:If match Condiction implies Next check NextLayor_Condiction Until Empty All Condictions implies Next act Promotion;系统实现4第22页，本讲稿共25页对时态规则生命周期：（1）(R1 S T1)U T2)（2）(R2 S T1)给出Java伪代码如下所示：（1）Always R1 Since T1 Until T2;（2）Always R2 Since T1;系统实现4第23页，本讲稿共25页本文对基于传统断言上时态逻辑断言规则推理进行了讨论并讨论了在工资智能决策系统中的时态问题。文中仅对工资决策规则中简单的一部分进行了设计、形式化描述与代码实现举例，这对系统实现具有指导意义，同时，这也为我们开发其他与时态有关的应用系统提供了一种思想。总结5第24页，本讲稿共25页The endThank you！请请老老师师同学同学批批评评指正！指正！第25页，本讲稿共25页