%0 Journal Article
%T 时态描述逻辑alc-ltl的tableau判定算法
%A 常亮
%A 王娟
%A 古天龙
%A 董荣胜？
%J 计算机科学
%D 2011
%X 时态描述逻辑alc-ltl将描述逻辑alc的描述能力与线性时态逻辑ltl的刻画能力结合起来，在具有较强描述能力的同时还使得可满足性问题保持在exptime-完全这个级别。针对alc-ltl缺少有效的判定算法的现状，将ltl的tableau判定算法与描述逻辑alc的推理机制有机地结合起来，给出了alc-ltl的tableau判定算法并证明了算法的可终止性、可靠性和完备性。该算法具有很好的可扩展性。当alc-工`i'i、中的描述逻辑从alc改变为任何一个具有可判定性特征的描述逻辑x时，只需要对算法进行简单修改，就可以得到相应的时态描述逻辑x-ltl的tableau判定算法。
%K 时态描述逻辑
%K 线性时态逻辑
%K 可满足性问题
%K tablcau算法
%K 复杂度
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=110834&flag=1