ExpTime Tableaux for Using Sound Global Caching
ExpTime Tableaux for Using Sound Global Caching
复制标题
用于使用健全全局缓存的 ExpTime Tableaux
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Linh Anh Nguyen
中科院分区：
文献类型：
--
作者：
R. Goré;Linh Anh Nguyen
我们提出了一个简单的ExpTime（复杂性最优）的tableau决策过程的基础上和或图形与健全的全球缓存检查满足的概念w.r.t.在$mathcal{ALC}$中的TBox。我们的算法很容易实现，并提供了一个基础ExpTime（复杂性最优）基于表格的决策程序，许多模态和描述逻辑，各种优化技术可以应用。
We present a simple ExpTime (complexity-optimal) tableau decision procedure based on and-or graphs with sound global caching for checking satisfiability of a concept w.r.t. a TBox in $mathcal{ALC}$. Our algorithm is easy to implement and provides a foundation for ExpTime (complexity-optimal) tableau-based decision procedures for many modal and description logics, to which various optimisation techniques can be applied.