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 \(\mathcal{ALBO}\) and show that it provides a basis for decision procedures for this logic and numerous other description logics with full role negation. \(\mathcal{ALBO}\) is the extension of \(\mathcal{ALC}\) with the Boolean role operators, inverse of roles, domain and range restriction operators and it includes full support for nominals (individuals). \(\mathcal{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 \({\textsc{MetTeL}}\) system.
Chapter PDF
Similar content being viewed by others
References
Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F.: Description Logic Handbook. Cambridge Univ. Press, Cambridge (2003)
Baumgartner, P., Schmidt, R.A.: Blocking and other enhancements for bottom-up model generation methods. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 125–139. Springer, Heidelberg (2006)
De Nivelle, H., Pratt-Hartmann, I.: A resolution-based decision procedure for the two-variable fragment with equality. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 211–225. Springer, Heidelberg (2001)
De Nivelle, H., Schmidt, R.A., Hustadt, U.: Resolution-based methods for modal logics. Log. J. IGPL 8(3), 265–292 (2000)
Grädel, E., Kolaitis, P.G., Vardi, M.Y.: On the decision problem for two-variable first-order logic. Bull. Sect. Log. 3, 53–69 (1997)
Hustadt, U., Schmidt, R.A.: Issues of decidability for description logics in the framework of resolution. In: Caferra, R., Salzer, G. (eds.) Automated Deduction in Classical and Non-Classical Logics. LNCS (LNAI), vol. 1761, pp. 191–205. Springer, Heidelberg (2000)
Hustadt, U., Schmidt, R.A., Georgieva, L.: A survey of decidable first-order fragments and description logics. J. Relat. Methods Comput. Sci. 1, 251–276 (2004)
Hustadt, U., Tishkovsky, D., Wolter, F., Zakharyaschev, M.: Automated reasoning about metric and topology (System description). In: Fisher, M., van der Hoek, W., Konev, B., Lisitsa, A. (eds.) JELIA 2006. LNCS (LNAI), vol. 4160, pp. 490–493. Springer, Heidelberg (2006)
Lutz, C., Sattler, U.: The complexity of reasoning with Boolean modal logics. In: Advances in Modal Logics, vol. 3, CSLI Publ., Stanford (2002)
Massacci, F.: Decision procedures for expressive description logics with intersection, composition, converse of roles and role identity. In: Proc. IJCAI 2001, pp. 193–198. Morgan Kaufmann, San Francisco (2001)
Schmidt, R.A.: Developing modal tableaux and resolution methods via first-order resolution. In: Advances in Modal Logic, vol. 6, pp. 1–26. College Publ. (2006)
Schmidt, R.A., Hustadt, U.: Mechanised reasoning and model generation for extended modal logics. In: de Swart, H., Orłowska, E., Schmidt, G., Roubens, M. (eds.) Theory and Applications of Relational Structures as Knowledge Instruments. LNCS, vol. 2929, pp. 38–67. Springer, Heidelberg (2003)
Schmidt, R.A., Orlowska, E., Hustadt, U.: Two proof systems for Peirce algebras. In: Berghammer, R., Möller, B., Struth, G. (eds.) Relational and Kleene-Algebraic Methods in Computer Science. LNCS, vol. 3051, pp. 238–251. Springer, Heidelberg (2004)
Tobies, S.: Decidability Results and Practical Algorithms for Logics in Knowledge Representation. PhD dissertation, RWTH Aachen (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schmidt, R.A., Tishkovsky, D. (2007). Using Tableau to Decide Expressive Description Logics with Role Negation. In: Aberer, K., et al. The Semantic Web. ISWC ASWC 2007 2007. Lecture Notes in Computer Science, vol 4825. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76298-0_32
Download citation
DOI: https://doi.org/10.1007/978-3-540-76298-0_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-76297-3
Online ISBN: 978-3-540-76298-0
eBook Packages: Computer ScienceComputer Science (R0)