by Schmidt, R. A. and Tishkovsky, D.
Abstract:
This paper presents a tableau approach for deciding description logics outside the scope of OWL DL 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. 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 objects (nominals). ALBO is a very expressive description logic which is NExpTime complete and subsumes Boolean modal logic and the two-variable fragment of first-order logic. An important novelty is the use of a versatile, unrestricted blocking rule as a replacement for standard loop checking mechanisms implemented in description logic systems. Our decision procedure is implemented in the MetTeL system.
Reference:
Deciding ALBO with Tableau (Schmidt, R. A. and Tishkovsky, D.), In Proceedings of the 20th International Workshop on Description Logics (DL-2007) (Calvanese, D., Franconi, E., Haarslev, V., Lembo, D., Motik, B., Tessaris, S., Turhan, A. Y., eds.), Bozen-Bolzano University Press, 2007.
Bibtex Entry:
@INPROCEEDINGS{SchmidtTishkovskyDL07,
AUTHOR = {Schmidt, R. A. and Tishkovsky, D.},
YEAR = {2007},
TITLE = {Deciding {ALBO} with Tableau},
BOOKTITLE = {Proceedings of the 20th International Workshop on Description Logics (DL-2007)},
EDITOR = {Calvanese, D. and Franconi, E. and Haarslev, V. and Lembo, D. and Motik, B. and Tessaris, S. and Turhan, A. Y.},
PUBLISHER = {Bozen-Bolzano University Press},
ISBN = {978-88-6046-008-5},
PAGES = {135--146},
URL = {http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-250/paper_75.pdf},
ABSTRACT = {
This paper presents a tableau approach for deciding description
logics outside the scope of OWL DL 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.
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 objects (nominals). ALBO is a very expressive
description logic which is NExpTime complete and subsumes
Boolean modal logic and the two-variable fragment of first-order
logic. An important novelty is the use of a versatile,
unrestricted blocking rule as a replacement for standard loop
checking mechanisms implemented in description logic systems.
Our decision procedure is implemented in the MetTeL system.
},
}