A Tableau Decision Procedure for $\mathcal{SHOIQ}$
A Tableau Decision Procedure for $\mathcal{SHOIQ}$
复制标题
DOI：
10.1007/s10817-007-9079-9
复制
发表时间：
2007-10
期刊：
影响因子：
--
通讯作者：
Ian Horrocks;U. Sattler
中科院分区：
文献类型：
--
作者：
Ian Horrocks;U. Sattler
OWL DL是W3C推荐的一种新的本体语言，它基于表达性描述逻辑。虽然本体的一致性问题是已知的可判定的，到目前为止，还没有已知的“实用”的决策程序，也就是说，目标导向的程序，很可能执行良好的现实本体派生的问题。我们提出了这样一个决策过程，一个稍微更有表现力的逻辑比，扩展著名的算法，这是几个非常成功的实现的基础。
OWL DL, a new W3C ontology language recommendation, is based on the expressive description logic. Although the ontology consistency problem foris known to be decidable, up to now there has been no known “practical” decision procedure, that is, a goal-directed procedure that is likely to perform well with realistic ontology derived problems. We present such a decision procedure for, a slightly more expressive logic than, extending the well-known algorithm for, which is the basis for several highly successful implementations.