计算机科学 ›› 2011, Vol. 38 ›› Issue (8): 150-154.

• 软件工程 • 上一篇    下一篇

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

常亮,王娟,古天龙,董荣胜   

  1. (桂林电子科技大学计算机科学与工程学院 桂林541004)
  • 出版日期:2018-11-16 发布日期:2018-11-16
  • 基金资助:
    本文受国家自然科学基金(60903079,60963010),广西自然科学基金(0832006G)资助。

Tableau Decision Algorithm for the Temporal Description Logic ALC-LTL

CHANG Liang , WANG Juan,GU Tian-long,DONG Rong-sheng   

  • Online:2018-11-16 Published:2018-11-16

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

关键词: 时态描述逻辑,线性时态逻辑,可满足性问题,Tablcau算法,复杂度

Abstract: As a combination of the description logic ALC and the linear temporal logic LTL, the temporal description logic ALC-LTL not only offers considerable expressive power going beyond both ALC and LTL, but also makes the satisfiability problem of it preserved to be EXPTIME-complete;however,an efficient decision algorithm for ALC-LTL is still absent Based on a combination of the Tableau algorithm of LTL and the reasoning mechanism provided by ALC,this paper presented a Tablcau decision algorithm for the logic ALC-L TL and proved that this algorithm is terminating,sound and complete. hhis algorithm enjoys excellent expandability; when the ALC component in the logic ALC-LTL is substituted by any other description logic X which is still decidable, this algorithm can be easily modified to act as a Tablcau decision algorithm for the corresponding temporal description logic X-LTL.

Key words: Temporal description logic, Linear temporal logic, Satisfiability problem, Tableau algorithm, Complexity

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!