时态描述逻辑alc-ltl的tableau判定算法

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