时态描述逻辑ALC-LTL的Tableau判定算法  

Tableau Decision Algorithm for the Temporal Description Logic ALC-LTL

作　　者：常亮[1] 王娟[1] 古天龙[1] 董荣胜[1] 

机构地区：[1]桂林电子科技大学计算机科学与工程学院,桂林541004

出　　处：《计算机科学》2011年第8期150-154,共5页Computer Science

基　　金：国家自然科学基金(60903079;60963010);广西自然科学基金(0832006Z)资助

摘　　要：时态描述逻辑ALC-LTL将描述逻辑ALC的描述能力与线性时态逻辑LTL的刻画能力结合起来,在具有较强描述能力的同时还使得可满足性问题保持在EXPTIME-完全这个级别。针对ALC-LTL缺少有效的判定算法的现状,将LTL的Tableau判定算法与描述逻辑ALC的推理机制有机地结合起来,给出了ALC-LTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性。该算法具有很好的可扩展性。当ALC-LTL中的描述逻辑从ALC改变为任何一个具有可判定性特征的描述逻辑X时,只需要对算法进行简单修改,就可以得到相应的时态描述逻辑X-LTL的Tableau判定算法。As a combination of the description logic ALC and the linear temporal logic LTL,the temporal description logic ALC-LTL not only offers considerable expressive power going beyond both ALC and LTL,but also makes the sa-tisfiability problem of it preserved to be EXPTIME-complete;however,an efficient decision algorithm for ALC-LTL is still absent.Based on a combination of the Tableau algorithm of LTL and the reasoning mechanism provided by ALC,this paper presented a Tableau decision algorithm for the logic ALC-LTL and proved that this algorithm is terminating,sound and complete.This algorithm enjoys excellent expandability;when the ALC component in the logic ALC-LTL is substituted by any other description logic X which is still decidable,this algorithm can be easily modified to act as a Tableau decision algorithm for the corresponding temporal description logic X-LTL.

关 键 词：时态描述逻辑 线性时态逻辑 可满足性问题 TABLEAU算法 复杂度 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]