A resolution-based decision procedure for SHOIQ

被引：0
作者：
Kazakov, Yevgeny [1 ]
Motik, Boris [1 ]
机构：
[1] Univ Oxford, Comp Lab, Oxford OX1 2JD, England
来源：
JOURNAL OF AUTOMATED REASONING | 2008年 / 40卷 / 2-3期
基金：
英国工程与自然科学研究理事会;
关键词：
description logics; resolution decision procedures; nominals;
D O I：
10.1007/s10817-007-9090-1
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We present a resolution-based decision procedure for the description logicQ1SHOIQ-the logic underlying the Semantic Web ontology language OWLDL. Our procedure is goal-oriented, and it naturally extends a similar procedure for SHIQ, which has proven itself in practice. Extending this procedure to SHOIQ using existing techniques is not straightforward because of nominals, number restrictions, and inverse roles - a combination known to cause termination problems. We overcome this difficulty by using the basic superposition calculus extended with custom simplification rules.
引用
收藏
页码：89 / 116
页数：28
相关论文
共 48 条
[1]  
[Anonymous], 2000, LOG J IGPL
[2]  
[Anonymous], 2004, Proceedings of KR
[3]  
ARMANDO A, 2001, LNCS, V2142, P549
[4]  
Baader F., 2003, DESCRIPTION LOGIC HD
[5]  
Baader F., 1998, TERM REWRITING ALL
[6]  
Bachmair L., 1994, Journal of Logic and Computation, V4, P217, DOI 10.1093/logcom/4.3.217
[7]   BASIC PARAMODULATION [J].
BACHMAIR, L ;
GANZINGER, H ;
LYNCH, C ;
SNYDER, W .
INFORMATION AND COMPUTATION, 1995, 121 (02) :172-192
[8]  
Bachmair L., 2001, HDB AUTOMATED REASON, VI, P19, DOI DOI 10.1016/B978-044450813-3/50004-7
[9]  
BACHMAIR L, 1993, LNCS, V713, P83
[10]  
Baumgartner P, 2006, LECT NOTES ARTIF INT, V4130, P125
12345