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

摘要

时态描述逻辑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 satisfiability 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.