Abstract
Description logics are a family of knowledge representation formalisms that are descended from semantic networks and frames via the system KL-ONE. During the last decade, it has been shown that the important reasoning problems (like subsumption and satisfiability) in a great variety of description logics can be decided using tableau-like algorithms. This is not very surprising since description logics have turned out to be closely related to propositional modal logics and logics of programs (such as propositional dynamic logic), for which tableau procedures have been quite successful.
Nevertheless, due to different underlying intuitions and applications, most description logics differ significantly from run-of-the-mill modal and program logics. Consequently, the research on tableau algorithms in description logics led to new techniques and results, which are, however, also of interest for modal logicians. In this article, we will focus on three features that play an important rôle in description logics (number restrictions, terminological axioms, and role constructors), and show how they can be taken into account by tableau algorithms.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baader, F.: Augmenting concept languages by transitive closure of roles: An alternative to terminological cycles. In: Proc. of IJCAI 1991, Sydney, Australia (1991)
Baader, F., Buchheit, M., Hollunder, B.: Cardinality restrictions on concepts. Artificial Intelligence 88(1-2), 195–213 (1996)
Baader, F., Bürckert, H.-J., Nebel, B., Nutt, W., Smolka, G.: On the expressivity of feature logics with negation, functional uncertainty, and sort equations. J. of Logic, Language and Information 2, 1–18 (1993)
Baader, F., Hanschke, P.: A schema for integrating concrete domains into concept languages. Technical Report RR-91-10, DFKI, Kaiserslautern, Germany, An abridged version appeared in Proc. of IJCAI 1991 (1991)
Baader, F., Hollunder, B.: A terminological knowledge representation system with complete inference algorithm. In: Boley, H., Richter, M.M. (eds.) PDK 1991. LNCS, vol. 567, pp. 67–86. Springer, Heidelberg (1991)
Baader, F., Hollunder, B., Nebel, B., Profitlich, H.-J., Franconi, E.: An empirical analysis of optimization techniques for terminological representation systems. In: Proc. of KR 1992, pp. 270–281. Morgan Kaufmann, San Francisco (1992)
Baader, F., Sattler, U.: Expressive number restrictions in description logics. J. of Logic and Computation 9(3), 319–350 (1999)
Borgida, A., Patel-Schneider, P.F.: A semantics and complete algorithm for subsumption in the CLASSIC description logic. J. of Artificial Intelligence Research 1, 277–308 (1994)
Brachman, R.J.: Reducing CLASSIC to practice: Knowledge representation meets reality. In: Proc. of KR 1992, pp. 247–258. Morgan Kaufmann, San Francisco (1992)
Brachman, R.J., Levesque, H.J.: The tractability of subsumption in frame-based description languages. In: Proc. of AAAI 1984, pp. 34–37 (1984)
Brachman, R.J., Levesque, H.J. (eds.): Readings in Knowledge Representation. Morgan Kaufmann, San Francisco (1985)
Brachman, R.J., Schmolze, J.G.: An overview of the KL-ONE knowledge representation system. Cognitive Science 9(2), 171–216 (1985)
Bresciani, P., Franconi, E., Tessaris, S.: Implementing and testing expressive description logics: Preliminary report. Working Notes of the 1995 Description Logics Workshop, Technical Report, RAP 07.95, Dip. di Inf. e Sist., Univ. di Roma La Sapienza", pp. 131–139, Rome, Italy (1995)
Buchheit, M., Donini, F.M., Schaerf, A.: Decidable reasoning in terminological knowledge representation systems. J. of Artificial Intelligence Research 1, 109–138 (1993)
Giacomo, G.D.: Decidability of Class-Based Knowledge Representation Formalisms. PhD thesis, Dip. di Inf. e Sist., Univ. di Roma La Sapienza (1995)
De Giacomo, G., Lenzerini, M.: Boosting the correspondence between description logics and propositional dynamic logics. In: Proc. of AAAI 1994, pp. 205–212. AAAI Press/The MIT Press (1994)
De Giacomo, G., Lenzerini, M.: Concept language with number restrictions and fixpoints, and its relationship with μ-calculus. In: Cohn, A.G. (ed.) Proc. of ECAI 1994, pp. 411–415. John Wiley & Sons, Chichester (1994)
De Giacomo, G., Lenzerini, M.: TBox and ABox reasoning in expressive description logics. In: Aiello, L.C., Doyle, J., Shapiro, S.C. (eds.) Proc. of KR 1996, pp. 316–327. Morgan Kaufmann, San Francisco (1996)
Donini, F.M., Hollunder, B., Lenzerini, M., Spaccamela, A.M., Nardi, D., Nutt, W.: The complexity of existential quanti fication in concept languages. Artificial Intelligence 2-3, 309–327 (1992)
Donini, F.M., Lenzerini, M., Nardi, D., Nutt, W.: The complexity of concept languages. In: Allen, J., Fikes, R., Sandewall, E. (eds.) Proc. of KR 1991, pp. 151–162. Morgan Kaufmann, San Francisco (1991)
Donini, F.M., Lenzerini, M., Nardi, D., Nutt, W.: Tractable concept languages. In: Proc. of IJCAI 1991, Sydney, pp. 458–463 (1991)
Giacomo, G.D., Massacci, F.: Tableaux and algorithms for propositional dynamic logic with converse. In: Proc. of CADE 1996, pp. 613–628 (1996)
Hanschke, P.: Specifying role interaction in concept languages. In: Proc. of KR 1992, pp. 318–329. Morgan Kaufmann, San Francisco (1992)
Hollunder, B.: Hybrid inferences in KL-ONE-based knowledge representation systems. In: Proc. of GWAI 1990. Informatik-Fachberichte, vol. 251, pp. 38–47. Springer, Heidelberg (1990)
Hollunder, B.: Consistency checking reduced to satisfiability of concepts in terminological systems. Annals of Mathematics and Artificial Intelligence 18(2-4), 133–157 (1996)
Hollunder, B., Baader, F.: Qualifying number restrictions in concept languages. In: Proc. of KR 1991, pp. 335–346 (1991)
Hollunder, B., Nutt, W.: Subsumption algorithms for concept languages. Technical Report RR-90-04, DFKI, Kaiserslautern, Germany (1990)
Hollunder, B., Nutt, W., Schmidt-Schauß, M.: Subsumption algorithms for concept description languages. In: Proc. of ECAI 1990, London, pp. 348–353. Pitman (1990)
Horrocks, I.: The FaCT system. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 307–312. Springer, Heidelberg (1998)
Horrocks, I.: Using an expressive description logic: FaCT or fiction? In: Proc. of KR 1998, pp. 636–647 (1998)
Horrocks, I., Patel-Schneider, P.F.: Optimizing description logic subsumption. J. of Logic and Computation 9(3), 267–293 (1999)
Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierarchies. J. of Logic and Computation 9(3), 385–410 (1999)
Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for expressive description logics. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol. 1705. Springer, Heidelberg (1999)
Lutz, C.: Complexity of terminological reasoning revisited. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol. 1705. Springer, Heidelberg (1999)
MacGregor, R.: The evolving technology of classification-based knowledge representation systems. In: Sowa, J.F. (ed.) Principles of Semantic Networks, pp. 385–400. Morgan Kaufmann, San Francisco (1991)
Mays, E., Dionne, R., Weida, R.: K-REP system overview. SIGART Bulletin 2(3) (1991)
Minsky, M.: A framework for representing knowledge. In: Haugeland, J. (ed.) Mind Design. The MIT Press, Cambridge (1981); Republished in [11]
Nebel, B. (ed.): Reasoning and Revision in Hybrid Representation Systems. LNCS, vol. 422. Springer, Heidelberg (1990)
Nebel, B.: Terminological reasoning is inherently intractable. Artificial Intelligence 43, 235–249 (1990)
Nebel, B.: Terminological cycles: Semantics and computational properties. In: Sowa, J.F. (ed.) Principles of Semantic Networks, pp. 331–361. Morgan Kaufmann, San Francisco (1991)
Patel-Schneider, P.F.: DLP. In: Proc. of DL 1999, CEUR Electronic Workshop Proceedings, pp. 9–13 (1999), http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-22/
Patel-Schneider, P.F., McGuiness, D.L., Brachman, R.J., Resnick, L.A., Borgida, A.: The CLASSIC knowledge representation system: Guiding principles and implementation rational. SIGART Bulletin 2(3), 108–113 (1991)
Peltason, C.: The BACK system - an overview. SIGART Bulletin 2(3), 114–119 (1991)
Quillian, M.R.: Word concepts: A theory and simulation of some basic capabilities. Behavioral Science 12, 410–430 (1967); Republished in [11]
Sattler, U.: A concept language extended with different kinds of transitive roles. In: Görz, G., Hölldobler, S. (eds.) KI 1996. LNCS (LNAI), vol. 1137. Springer, Heidelberg (1996)
Savitch, W.J.: Relationship between nondeterministic and deterministic tape complexities. J. of Computer and System Science 4, 177–192 (1970)
Schild, K.: A correspondence theory for terminological logics: Preliminary report. In: Proc. of IJCAI 1991, Sydney, Australia, pp. 466–471 (1991)
Schild, K.: Terminological cycles and the propositional μ-calculus. In: Doyle, J., Sandewall, E., Torasso, P. (eds.) Proc. of KR 1994, Bonn, pp. 509–520. Morgan Kaufmann, San Francisco (1994)
Schmidt-Schauß, M.: Subsumption in KL-ONE is undecidable. In: Brachman, R.J., Levesque, H.J., Reiter, R. (eds.) Proc. of KR 1989, pp. 421–431. Morgan Kaufmann, San Francisco (1989)
Schmidt-Schauß, M., Smolka, G.: Attributive concept descriptions with complements. Artificial Intelligence 48(1), 1–26 (1991)
Spaan, E.: The complexity of propositional tense logics. In: de Rijke, M. (ed.) Diamonds and Defaults, pp. 287–307. Kluwer Academic Publishers, Dordrecht (1993)
Tobies, S.: A PSPACE algorithm for graded modal logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 52–66. Springer, Heidelberg (1999)
Van der Hoek, W., De Rijke, M.: Counting objects. J. of Logic and Computation 5(3), 325–345 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baader, F., Sattler, U. (2000). Tableau Algorithms for Description Logics. In: Dyckhoff, R. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2000. Lecture Notes in Computer Science(), vol 1847. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722086_1
Download citation
DOI: https://doi.org/10.1007/10722086_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67697-3
Online ISBN: 978-3-540-45008-5
eBook Packages: Springer Book Archive