摘要: 时态描述逻辑ALC-LTL将描述逻辑ALC的描述能力与线性时态逻辑LTL的刻画能力结合起来,在具有较强描述能力的同时还使得可满足性问题保持在EXPTIME-完全这个级别。针对ALC-LTL缺少有效的判定算法的现状,将LTL的Tableau判定算法与描述逻辑ALC的推理机制有机地结合起来,给出了ALC-LTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性。该算法具有很好的可扩展性。当ALC-工`I'I、中的描述逻辑从ALC改变为任何一个具有可判定性特征的描述逻辑X时,只需要对算法进行简单修改,就可以得到相应的时态描述逻辑X-LTL的Tableau判定算法。
常亮,王娟,古天龙,董荣胜. 时态描述逻辑ALC-LTL的Tableau判定算法[J]. 计算机科学, 2011, 38(8): 150-154. https://doi.org/
CHANG Liang , WANG Juan,GU Tian-long,DONG Rong-sheng. Tableau Decision Algorithm for the Temporal Description Logic ALC-LTL[J]. Computer Science, 2011, 38(8): 150-154. https://doi.org/