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

摘要：

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

关键词：时态描述逻辑、线性时态逻辑、可满足性问题、Tableau算法、复杂度

所属期刊栏目：38

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金60903079,60963010;广西自然科学基金0832006Z

在线出版日期：2012-01-14（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：150-154