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

时态描述逻辑ALC-LTL将描述逻辑ALC的描述能力与线性时态逻辑LTL的刻画能力结合起来，在具有较强描述能力的同时还使得可满足性问题保持在EXPTIME-完全这个级别。针对ALC-LTL缺少有效的判定算法的现状，将LTL的Tableau判定算法与描述逻辑ALC的推理机制有机地结合起来，给出了ALC-LTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性。该算法具有很好的可扩展性。当ALC-工`I'I、中的描述逻辑从ALC改变为任何一个具有可判定性特征的描述逻辑X时，只需要对算法进行简单修改，就可以得到相应的时态描述逻辑X-LTL的Tableau判定算法。