文档介绍：学号桂林电子科技大学硕硕硕硕士士士士学学学学位位位位论论论论文文文文题目时态描述逻辑ALC-LTL的推理及应用研究(英文)ResearchonReasoningMechanismsandApplicationsoftheTemporalDescriptionLogicALC-LTL研究生学号::::092031103研究生姓名::::王娟指导教师姓名、职务::::常亮(教授)申请学位门类::::工学硕士学科、专业::::计算机应用技术提交论文日期::::2012年4月论文答辩日期::::2012年6月10日2012年6月10日独创性((((或创新性))))声明本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知,除了文中特别加以标注和致谢中所罗列的内容以外,论文中不包含其他人已经发表或撰写过的研究成果;也不包含为获得桂林电子科技大学或其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中做了明确的说明并表示了谢意。申请学位论文与资料若有不实之处,本人承担一切相关责任。本人签名:日期:关于论文使用授权的说明本人完全了解桂林电子科技大学有关保留和使用学位论文的规定,即:研究生在校攻读学位期间论文工作的知识产权单位属桂林电子科技大学。本人保证毕业离校后,发表论文或使用论文工作成果时署名单位仍然为桂林电子科技大学。学校有权保留送交论文的复印件,允许查阅和借阅论文;学校可以公布论文的全部或部分内容,可以允许采用影印、缩印或其它复制手段保存论文。(保密的论文在解密后遵守此规定)本学位论文属于保密在____年解密后适用本授权书。本人签名:日期:导师签名:摘要I摘要描述逻辑是一类适合于刻画静态领域知识的逻辑语言,在当前成为研究热点的语义Web中扮演着关键角色,是W3C推荐的Web本体语言OWL的逻辑基础。描述逻辑的主要特点在于具有较强描述能力的同时还具有可判定性特征,并且具有高效的推理算法和推理工具作为支撑。为了将描述逻辑的刻画能力从静态领域扩展到动态领域,研究者提出了描述逻辑的各种扩展形式。其中,FranzBaader教授提出的时态描述逻辑ALC-LTL将描述逻辑ALC与线性时态逻辑LTL结合了起来,同时使得可满足性问题保持在EXPTIME-完全这个级别。为了进一步发挥ALC-LTL的知识表达和推理能力。首先,需要为其设计可靠和完备的判定算法;其次,需要开发有效的推理工具;最后,需要给出一些典型的应用实例。本文基于这一思路开展研究工作,完成的工作主要如下:(1)针对ALC-LTL缺少有效的判定算法的现状,给出了ALC-LTL的Tableau判定算法并对其性质进行了证明。该算法首先利用相关扩展规则分别对不存在后继状态的伪状态和饱和状态进行扩展;其次删除所有的伪状态;最后删除不满足要求的饱和状态。如果能生成Tableau,则所判定的公式是可满足的,否则是不可满足的,从而实现了对ALC-LTL公式的可满足性判定。(2)为了能够快速准确的对ALC-LTL公式的可满足性进行判定,在ALC-LTL的Tableau判定算法基础上,开发出相应的ALC-LTL(Tableau)推理机软件。软件每次只对Tableau的一条分支进行判定,如果存在一条可满足的分支,则返回结果为该公式是可满足的;如果所判定的分支存在冲突或者可能性断言没有被实现,才对下一条分支进行判定,如果所有分支都不可满足,返回结果为该公式是不可满足的,否则返回结果为该公式是可满足的。(3)针对语义Web服务是对动态知识的推理,将ALC-LTL应用于语义Web服务的验证中。首先,从OWL-S中的ProcessModel出发,对于服务组合中每一个原子服务,将其对应的原子过程的输入、输出、前提条件、局部变量以及结果分别用ALC-LTL来刻画;其次,对组合服务进行建模,并且对其推理问题进行全面刻画,将对服务的推理问题转化为对逻辑公式的可满足性判定问题,从而实现对服务组合的可执行性以及投影问题的验证;最后对服务组合实例进行验证分析。关键词:ALC-LTL;Tableau;可满足性问题;语义Web服务;OWL-SAbstractIIAbstractDescriptionlogicisakindoflogiclanguagesuitablefordepictingtheknowledgeofstaticfield,whichplaysakeyroleinsemanticWeb,,butalsohavehigh-effi