%0 Conference Paper %1 Tishkovsky/2007/Using %A Tishkovsky, Dmitry %A Schmidt, Renate %B Proceedings of the 6th International Semantic Web Conference and 2nd Asian Semantic Web Conference (ISWC/ASWC2007), Busan, South Korea %C Berlin, Heidelberg %D 2007 %E Aberer, Karl %E Choi, Key-Sun %E Noy, Natasha %E Allemang, Dean %E Lee, Kyung-Il %E Nixon, Lyndon J B %E Golbeck, Jennifer %E Mika, Peter %E Maynard, Diana %E Schreiber, Guus %E Cudré-Mauroux, Philippe %I Springer Verlag %K 2007 description expressive formal_language iswc logic negation reasoning research_07 role semantic_web tableau using %P 435--448 %T Using Tableau to Decide Expressive Description Logics with Role Negation %U http://iswc2007.semanticweb.org/papers/435.pdf %V 4825 %X 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 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 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. An implementation of our approach exists in the MetTeL system.

@inproceedings{Tishkovsky/2007/Using, 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 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 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. An implementation of our approach exists in the MetTeL system.}, added-at = {2007-11-07T19:13:58.000+0100}, address = {Berlin, Heidelberg}, author = {Tishkovsky, Dmitry and Schmidt, Renate}, biburl = {https://www.bibsonomy.org/bibtex/2ecf039b215423eb7e62b423c15278414/iswc2007}, booktitle = {Proceedings of the 6th International Semantic Web Conference and 2nd Asian Semantic Web Conference (ISWC/ASWC2007), Busan, South Korea}, crossref = {http://data.semanticweb.org/conference/iswc-aswc/2007/proceedings}, editor = {Aberer, Karl and Choi, Key-Sun and Noy, Natasha and Allemang, Dean and Lee, Kyung-Il and Nixon, Lyndon J B and Golbeck, Jennifer and Mika, Peter and Maynard, Diana and Schreiber, Guus and Cudré-Mauroux, Philippe}, interhash = {e74efa71b2a3da90ce5fa275aca9461a}, intrahash = {ecf039b215423eb7e62b423c15278414}, keywords = {2007 description expressive formal_language iswc logic negation reasoning research_07 role semantic_web tableau using}, month = {November}, pages = {435--448}, publisher = {Springer Verlag}, series = {LNCS}, timestamp = {2007-11-07T19:20:54.000+0100}, title = {Using Tableau to Decide Expressive Description Logics with Role Negation}, url = {http://iswc2007.semanticweb.org/papers/435.pdf}, volume = 4825, year = 2007 }