by Schmidt, R. A. and Tishkovsky, D.
Abstract:
This paper presents a tableau approach for deciding description logics outside the scope of OWL DL/1.1 and current state-of-the-art tableau-based description logic systems. In particular, we define a sound and complete tableau calculus for the description logic ALBO and show that it provides a basis for decision procedures for this logic and numerous other description logics with full role negation. ALBO is the extension of ALC with the Boolean role operators, inverse of roles, domain and range restriction operators and it includes full support for nominals (individuals). ALBO is a very expressive description logic which subsumes Boolean modal logic and the two-variable fragment of first-order logic and reasoning in it is NExpTime-complete. An important novelty is the use of a generic, unrestricted blocking rule as a replacement for standard loop checking mechanisms implemented in description logic systems. An implementation of our approach exists in the MetTeL system.
Reference:
Using Tableau to Decide Expressive Description Logics with Role Negation (Schmidt, R. A. and Tishkovsky, D.), In The Semantic Web, 6th International Semantic Web Conference, 2nd Asian Semantic Web Conference, ISWC 2007 + ASWC 2007, Busan, Korea, November 11–15, 2007 (Aberer, K., Choi, K.-S., Fridman Noy, N., Allemang, D., Lee, K.-I., Nixon, L. J. B., Golbeck, J., Mika, P., Maynard, D., Mizoguchi, R., Schreiber, G., Cudré-Mauroux, P., eds.), Springer, volume 4825, 2007.
Bibtex Entry:
@INPROCEEDINGS{SchmidtTishkovsky07b,
AUTHOR = {Schmidt, R. A. and Tishkovsky, D.},
YEAR = {2007},
TITLE = {Using Tableau to Decide Expressive Description Logics with Role Negation},
EDITOR = {Aberer, K. and Choi, K.-S. and Fridman Noy, N. and Allemang, D. and Lee, K.-I. and Nixon, L. J. B. and Golbeck, J. and Mika, P. and Maynard, D. and Mizoguchi, R. and Schreiber, G. and Cudr{\'e}-Mauroux, P.},
BOOKTITLE = {The Semantic Web, 6th International Semantic Web Conference, 2nd Asian Semantic Web Conference, ISWC 2007 + ASWC 2007, Busan, Korea, November 11--15, 2007},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4825},
PUBLISHER = {Springer},
PAGES = {438--451},
DOI = {http://dx.doi.org/10.1007/978-3-540-76298-0_32},
URL ={http://www.springerlink.com/content/t8660444032w906t/fulltext.pdf},
ABSTRACT = {
This paper presents a tableau approach for deciding description
logics outside the scope of OWL DL/1.1 and current state-of-the-art
tableau-based description logic systems. In particular, we
define a sound and complete tableau calculus for the description
logic ALBO and show that it provides a basis for decision
procedures for this logic and numerous other description logics
with full role negation.
ALBO is the extension of ALC with the Boolean role operators,
inverse of roles, domain and range restriction operators and it includes full
support for nominals (individuals). ALBO is a very expressive
description logic which subsumes Boolean modal logic and the
two-variable fragment of first-order logic and reasoning in it is
NExpTime-complete.
An important novelty is the use of a generic,
unrestricted blocking rule as a replacement for standard loop
checking mechanisms implemented in description logic systems.
An implementation of our approach exists in the MetTeL system.
}
}