Knowledge Representation - Description Logics

Description Logics

Knowledge Representation is the field of Artificial Intelligence which focuses on the design of formalisms that are both epistemologically and computationally adequate for expressing knowledge on a particular domain. One of the main research lines of the field has been concerned with the idea that the knowledge should be represented by characterizing classes of objects and the relationship among them. The organization of the classes used to describe a domain of interest is based on a hierarchical structure, which not only provides an effective and compact representation of information, but also allows for performing the relevant reasoning tasks in a computationally effective way.

The above principle was underlying the development of the first frame systems and semantic networks. However, such systems were in general not formally defined and the associated reasoning tools were strongly dependent on the implementation strategies. A fundamental step towards a logic-based characterization of such systems has been accomplished through the work on the KL-ONE system, which collected many of the ideas stemming from earlier semantic networks and frame-based systems, and provided a logical basis for interpreting objects, classes (or concepts), and relationships (or links, or roles) between them. The first goal of such a logical reconstruction was the precise characterization of the set of constructs used to build class and link expressions. The second goal was to provide reasoning procedures that are sound and complete with respect to the semantics. The article ``The tractability of subsumption in Frame-Based Description Languages'' by R. Brachman and H. Levesque, addressing the tradeoff between the expressivity of KL-ONE like languages and the computational complexity of reasoning, is usually regarded as the origin for the research on Description Logics.

The research in the area of Description Logics has thereafter begun under the label terminological systems to emphasize the fact that classes and relationships were used to establish the basic terminology adopted in the modeled domain. Later, the emphasis was on the set of concept forming constructs admitted in the language, giving rise to the name concept languages. In the past years, after the attention has been further moved towards the properties of the underlying logical systems, the term Description Logics has become popular.

The research on Description Logics has covered theoretical aspects, implementation of knowledge representation systems (modern frame-based systems) and the realization of applications by means of such systems in several areas. This kind of development has been recognized by the Artificial Intelligence community as one example to follow, as far as the methodology of research development is concerned. The key element has been the a very close interaction between theory and practice. On the one hand, there are various implemented systems based on description logics, which offer a palette of description formalisms with differing expressive power, and which are employed in various application domains (such as natural language processing, configuration of technical systems, databases). On the other hand, the formal and computational properties (like decidability, complexity) of various description formalisms are investigated in detail. These investigations are usually motivated by the use of certain constructors in systems or the need for these constructors in specific applications and the results have influenced the design of new systems.

The Description Logics research community currently consists of at least 100 active researchers, the largest groups being in Germany, Italy, and the USA. In addition, other communities are now becoming interested in Description Logics, most notably the Data Base one.

After more than decade of research there is a substantial body of work and well-established material to provide a systematic introduction to the subject. However, a comprehensive introduction to Description Logics is still missing, and neither survey papers available in the literature, nor Workshop Proceedings are adequate for this purpose.

 

Complexity of reasoning in description logics

Note: the information provided on this page is (always) incomplete.
Base description logic (corresponds to the multi-modal logic K):

ALC ::=   ⊥  |  A  |  ¬C  |  C ∧ D  |  C ∨ D  |  ∃R.C  |  ∀R.C

Concept constructors:

F – functionality2: (≤1 R)
 N – (unqualified) number restrictions: (≥n R), (≤n R)
 Q – qualified number restrictions: (≥n R.C), (≤n R.C)
 O – nominals: {a} or {a1,...,an} ("one-of")
 

μ – least fixpoint operator: μX.C
 R⊆S – role-value-maps
 f = g – agreement of functional role chains ("same-as")

Role constructors:

I – role inverses: R—

∩ – role intersection3: R∩S
 ∪ – role union: R∪S
 ¬ – role complement:
o – role chain (composition): RoS
 * – reflexive-transitive closure4: R*
 id – concept identity: id(C)
 complex roles5 in number restriction6

TBox options:

Empty TBox
 Acyclic TBox (A≡C, A is a concept name; no cycles)
 General TBox (C⊆D for arbitrary concepts C and D)

Additional axioms (in RBox):

S – Transitivity axioms: Trans(R)
H – Role hierarchy axioms: R ⊆ S

You have selected the description logic: ALC 
Complexity of reasoning problems
Reasoning problem Complexity Comments and references
Concept satisfiability PSpace-complete
  • Hardness for ALC: see [54].
  • Upper bound for ALCQ: see [58, Theorem 4.6].
ABox consistency PSpace-complete Upper bound for ALCQO: see [5, Appendix A].
Important properties of the description logic
Finite model property Yes For all sublogics of ALCreg with any TBoxes; see [19, Theorem 3.2].
Tree model property Yes For all sublogics of ALCFIreg with any TBoxes; see [1, p.189, Theorem 5.6].



Notes:
  1. The letters O, I, and Q   are customary written in various order, e.g., ALCQIO, but SHOIQ . Here we do not reflect this tradition, but rather use a uniform naming scheme.
  2. The letter F is sometimes employed to express the presence of feature (dis)agreement constructor (see [1, pp.88,488], [37]), rather than functionality (see [5, 38, 28, 32]).
  3. The presence of role intersection operator is sometimes indicated by a letter R  , e.g. ALCNR := ALCN(∩).
  4. Transitive closure is usually denoted as R+. The operators * and + are expressible from each other via R+ = R o R* and R* = id(T) ∪ R+. Note however that the former definition is not linearly bounded. Therefore, any complexity result for a logic with + immediately implies the same result for a logic with (*,o), but not vice versa.

     
  5. In the selector "Allow/disallow complex roles in number restriction", a role (expression) is called complex if it contains any role operations. A logic name often does not indicate whether this assumption holds; for instance, in literature ALCQIreg usually denotes for the logic with only role names and their inverses inside number restrictions, whereas ALCN(o) refers to the logic allowing role composition within number restrictions. To avoid this ambiguity, the selector was introduced here explicitly.

     
  6. Another distinction is important for logics with unqualified number restrictions N and additional role operations: one can independently allow or disallow role operations in value restrictions (∃R.C and ∀R.C) and/or in number restrictions (≥n R). Strictly speaking, the naming of logics must look like ALC(∪,—)N(∪,o). However, the selectors displayed in the above table allow only for specifying logics in which either all role operators are allowed simultaneously in value and number restrictions, or some role operators are forbidden in number restrictions. Note that this suffices for logics with qualified number restrictions Q, since ∃R.C can be expressed as ≥1 R.C. As fo logics with N, we always state (in the comments) what holds in other cases.

     
  7. Final note: a symbol ☺ in the above table means that the author of this web page did not succeeded to find out in the literature any results concerning the logic under consideration. If you have any information about that logic, the author would be grateful if you send him a mail with the referrence. Sometimes, you can find out the desired complexity result using this tool by adding/removing some ingredients from the logic you consider, since it is not guaranteed that whenever this tool knows the complexity of two logics, and these complexities are the same, then the program knows the complexity of all logics in between. As already pointed out, this is always an incomplete version.
Additional sources
  1. Here you will find 6 diagrams depicting the complexity of concept satisfiability and ABox consistency problems for logics in between ALC and SHOIQ. There are some gaps (open problems?) in those diagrams!
  2. Here you will find a description of how ABox can be eliminated in presence of nominals (i.e., in extensions of ALCO) and how TBox can be eliminated in extensions of ALCIO, SH, and ALC(∪,*). Proofs are missing there so far (can be found in literature below).
  3. Here you will find local copies of all the papers listed below (for which an online version was available at all). The naming of files corresponds to the titles of the papers, so you will find a paper you need quickly.

References

  1. The Description Logic Handbook. Franz Baader, Diego Calvanese, Deborah L.McGuinness, Daniele Nardi, and Peter F. Patel-Schneider, editors. Cambridge University Press, 2003.
  2. Carlos Areces, Patrick Blackburn, and Maarten Marx. A road-map on complexity for hybrid logics. In Jörg Flum and Mario Rodrígues-Artalejo, editors, Computer Science Logic, number 1683 in Lecture Notes in Computer Science, pp.307-321, Springer-Verlag, 1999. Available here (ps.gz, ps, pdf).
  3. Franz Baader. Augmenting concept languages by transitive closure of roles: An alternative to terminological cycles. In Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI'91), 1991. Research report is available here (ps.gz).
  4. Franz Baader and Ulrike Sattler. Expressive number restrictions in Description Logics. Journal of Logic and Computation, 9(3):319-350, 1999. Available here (ps.gz).
  5. Franz Baader, Maja Milicic, Carsten Lutz, Ulrike Sattler, and Frank Wolter. Integrating Description Logics and Action Formalisms for Reasoning about Web Services. LTCS-Report 05-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005. Available here (ps.gz).
  6. Robert Berger. The undecidability of the dominoe problem. Memoirs of the American Mathematical Society, vol. 66, pp. 1–72, 1966.
  7. Martin Buchheit, Francesco M. Donini, and Andrea Schaerf. Decidable reasoning in terminological knowledge representation systems. J. of Artificial Intelligence Research, 1:109-138, 1993. Available here (ps, pdf).
  8. Martin Buchheit, Francesco M. Donini, and Andrea Schaerf. Decidable reasoning in terminological knowledge representation systems. Research Report RR-93-10, Deutsches Forschungszentrum für Künstliche Intelligenz (DFKI), Saarbrucken (Germany), 1993. Available here (ps.gz, ps, pdf). An abridged version appeared in Proc. of the 13th Int. Joint Conf. on Artificial Intelligence (IJCAI'93), pp.704-709. Morgan Kaufmann, Los Altos, 1993.
  9. Diego Calvanese. Finite model reasoning in Description Logics. In L.C.Aiello, Jon Doyle, and Stuart C.Shapiro, editors, Proc. of the 5th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR'96), pp.292-303. Morgan Kaufmann, Los Altos, 1996. Available here (ps.gz).
  10. Diego Calvanese. Unrestricted and finite model reasoning in class-based representation formalisms. PhD Thesis, Dipartimento di Informatica e Sistemistica, Università di Roma "La Sapienza", 1996. Available here (ps.gz) or here (ps.gz).
  11. Diego Calvanese, Giuseppe De Giacomo, and Maurizio Lenzerini. Reasoning in expressive Description Logics with fixpoints based on automata on infinite trees. In Proc. of the 16th Int. Joint Conf. on Artificial Intelligence (IJCAI'99), pp. 84–89, 1999. Available here (ps.gz) and here (pdf).
  12. Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, and Daniele Nardi. Reasoning in expressive Description Logics. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, pages 1581–1634 (Chapter 23). Elsevier Science Publishers, 2001. Available here (ps.gz).
  13. Ryszard Danecki. Nondeterministic Propositional Dynamic Logic with intersection is decidable. Proc. of the 5th Symposium on Computation Theory (Zaborów, Poland) (A. Skowron, editor), LNCS, vol. 208, Springer, December 1984, pp. 34–53.
  14. Giuseppe De Giacomo. Decidability of class-based knowledge representation formalisms. PhD Thesis, Dipartimento di Informatica e Sistemistica, Università di Roma "La Sapienza", 1995. Available here (ps.gz, ps, pdf).
  15. Giuseppe De Giacomo and Maurizio Lenzerini. Boosting the correspondence between Description Logics and propositional dynamic logics. In Proc. of the 12th Nat. Conf. on Artificial Intelligence (AAAI'94), pp.205-212. AAAI Press / The MIT Press, 1994. Available here (ps.gz, ps, pdf).
  16. Giuseppe De Giacomo and Maurizio Lenzerini. TBox and ABox reasoning in expressive Description Logics. In L.C.Aiello, Jon Doyle, and Stuart C.Shapiro, editors, Proc. of the 5th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR'96), pp.316-327. Morgan Kaufmann, Los Altos, 1996. Available here (ps.gz, ps, pdf).
  17. Giuseppe De Giacomo and Maurizio Lenzerini. A uniform framework for concept definitions in Description Logics. Journal of Artificial Intelligence Research (JAIR), vol. 6, pp. 87–110, 1997. Available here (ps, ps.Z, pdf).
  18. Francesco M. Donini and Fabio Massacci. EXPTIME tableaux for ALC. Artificial Intelligence, 124(1):87-138, 2000. Available here (ps.gz, ps, pdf). Extended abstract is available here (ps.gz, ps, pdf).
  19. Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. J. of Computer and System Science, 18:194-211, 1979. Available here (pdf).
  20. George Gargov, Solomon Passy, and Tinko Tinchev. Modal environment for Boolean speculations. In Dimiter G.Skordev, editor, Mathematical Logic and its Applications, pp. 253-263. Plenum Press, New York, 1987.
  21. Erich Grädel, Martin Otto, and Eric Rosen. Two variable logic with counting is decidable. In Proc. of the 12th IEEE Symp. on Logic in Computer Science (LICS'97), pp.306-317. IEEE Computer Society Press, 1997. Available here (ps, pdf).
  22. Fabio Grandi. On expressive number restrictions in Description Logics. In Proc. of the 2001 Int. Workshop on Description Logics (DL'2001), pp. 56–65, 2001. Available here (pdf) and here (ps).
  23. Fabio Grandi. On expressive Description Logics with composition of roles in number restrictions. In Proc. of the 9th Int. Conf. on Logic for Programming Artificial Intelligence and Reasoning (LPAR'2002), Tbilisi, Georgia, October 2002. Lecture Notes in Artificial Intelligence 2514, pp. 202–215, Berlin, Springer-Verlag, 2002. Available here (pdf). A Technical Report is available as pdf. An extended abstract is in Proc. of the 2002 Int. Workshop on Description Logics (DL'2002) and available here (ps).
  24. David Harel. Dynamic Logic. In D. Gabbay and F. Guenther, editors, Handbook of Philosophical Logic, vol. 2, pp. 497–604. Reidel, Dordrecht, Holland, 1984.
  25. Jan Hladik. A tableau system for the Description Logic SHIO. In Proc. of the Doctoral Programme of the 2nd Int. Joint Conf. on Automated Reasoning (IJCAR' 2004). Available here (ps).
  26. Jan Hladik and Jörg Model. Tableau systems for SHIO and SHIQ. In Proc. of the 2004 Int. Workshop on Description Logics (DL'2004). Available here (pdf).
  27. Wiebe van der Hoek. On the semantics of graded modalities. Journal of Applied Non-Classical Logics (JANCL), vol.2, num.1, 1992.
  28. Ian Horrocks and Ulrike Sattler. A Description Logic with transitive and inverse roles and role hierarchies. Journal of Logic and Computation, 9(3):385-410, 1999. Available here (pdf).
  29. Ian Horrocks and Ulrike Sattler. A tableaux decision procedure for SHOIQ. In Proc. of 19th Int. Joint Conf. on Artificial Intelligence (IJCAI'2005), 2005. Available here (pdf). Accompanying technical report is available (pdf).
  30. Ian Horrocks and Ulrike Sattler. Ontology reasoning in the SHOQ(D) Description Logic. In B. Nebel, editor, Proc. of the 17th Int. Joint Conf. on Artificial Intelligence (IJCAI 2001), pp. 199–204. Morgan Kaufmann, 2001. Available here (pdf) and here (ps).
  31. Ian Horrocks, Ulrike Sattler, and Stephan Tobies. Practical reasoning for expressive Description Logics. In Harald Ganzinger, David McAllester, and Andrei Voronkov, editors, Proc. of the 6th Int. Conference on Logic for Programming and Automated Reasoning (LPAR'99), number 1705 in Lecture Notes in Artificial Intelligence, pages 161-180. Springer-Verlag, 1999. Available here (pdf).
  32. Ian Horrocks, Ulrike Sattler, and Stephan Tobies. Practical reasoning for very expressive Description Logics. Logic Journal of the IGPL, 8(3):239-263, 2000. Available here (pdf)
  33. Dexter Kozen. Results on propositional μ-calculus. Theoretical Computer Science, vol. 33, pp. 333–354, 1983.
  34. Dexter Kozen. A finite model theorem for the propositional μ-calculus. Studia Logica, vol. 47, num. 3, pp. 233–241, 1988. Available here (pdf)
  35. Martin Lange. A lower complexity bound for Propositional Dynamic Logic with intersection. In Proc. of Advances in Modal Logic 2004 (AiML'04), Manchester, UK, 2004. University of Manchester Technical Report UMCS-04-09-01. Available here (ps.gz, pdf).
  36. Martin Lange and Carsten Lutz. 2-ExpTime lower bounds for Propositional Dynamic Logics with intersection. Journal of Symbolic Logic, 2005. Available here (ps.gz).
  37. Carsten Lutz. The complexity of Description Logic with concrete domains. PhD Thesis, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2002. Available here (ps.gz, pdf).
  38. Carsten Lutz. An improved NExpTime-hardness result for description logic ALC extended with inverse roles, nominals, and counting. LTCS-Report 04-07, Technical University Dresden, 2004. Available here (ps.gz, abstract).
  39. Carsten Lutz. PDL with intersection and converse is decidable. In Annual Conference of the European Association for Computer Science Logic (CSL'05), LNCS. Springer Verlag, 2005. Available here (ps.gz). Technical Report is available here (ps.gz).
  40. Carsten Lutz and Ulrike Sattler. The complexity of reasoning with Boolean Modal Logics. In Frank Wolter, Heinrich Wansing, Maarten de Rijke, and Michael Zakharyaschev, editors, Advances in Modal Logics, Volume 3. CSLI Publications, Stanford, 2001. Available here (ps.gz). Extended version is available here (ps.gz).
  41. Carsten Lutz, Ulrike Sattler, and Frank Wolter. Modal logics and the two-variable fragment. In Annual Conference of the European Association for Computer Science Logic (CSL'2001), LNCS, Paris, France, 2001. Springer Verlag. Available here (ps.gz).
  42. Carsten Lutz and Dirk Walther. PDL with negation of atomic programs. Journal of Applied Non-Classical Logic, 15(2):189-214, 2005. Available here (ps.gz). Technical Report is available here (ps.gz). A version published in Proc. of the 2nd Int. Joint Conf. on Automated Reasoning (IJCAR'2004), Lecture Notes in Artificial Intelligence. Springer Verlag, 2004 — is available here (ps.gz).
  43. Fabio Massacci. Decision procedures for expressive Description Logics with intersection, composition, converse of roles and role identity. In Proc. of the 17th Int. Joint Conf. on Artificial Intelligence (IJCAI'2001), pp.193-198, 2001. Available here (pdf).
  44. Ralf Molitor. Konsistenz von Wissensbasen in Beschreibungslogiken mit Rollenoperatoren. Diploma thesis, RWTH Aachen, Germany, 1997. (in German). Available here (ps.gz).
  45. Leszek Pacholski, Wieslaw Szwast, Lidia Tendera. Complexity of two-variable logic with counting. In Proc. of the 12th IEEE Symp. on Logic in Computer Science (LICS'97), pp.318-327. IEEE Computer Society Press, 1997. Available here (ps.gz, ps, pdf).
  46. Jeff Z. Pan and Ian Horrocks. Semantic Web ontology reasoning in the SHOQ(Dn) Description Logic. In Proc. of the 2002 Description Logic Workshop (DL'2002), vol. 63 of CEUR, pp. 53–62, 2002. Available here (pdf).
  47. Vaughan Pratt. Models of program logics. In Proc. of the 20th Annual Symp. on the Foundations of Computer Science (FOCS'79), pp.115-122, 1979.
  48. Maarten de Rijke. A note on graded modal logic. Studia Logica, 64(2):271-283, 2000. Available here (ps, pdf).
  49. Raphael Robinson. Undecidability and nonperiodicity of tilings on the plane. Inventiones Math., vol. 12, pp. 177–209, 1971.
  50. Ulrike Sattler and Moshe Y. Vardi. The hybrid μ-calculus. In R. Gore, A. Leitsch, and T. Nipkow, editors, Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR'2001), vol. 2083 of LNAI, pp. 76–91. Springer Verlag, 2001. Available here (ps.gz).
  51. Andrea Schaerf. Reasoning with individuals in concept languages. Data and Knowlegde Engineering, 13(2):141-176, 1994. Available here (ps, abstract).
  52. Klaus Schild. A correspondence theory for terminological logics: Preliminary report. In Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI'91), pp.466-471, 1991. Available here (pdf, ps.gz).
  53. Klaus Schild. Towards a theory of frames and rules. Technical report, Fachbereich Informatik, Technische Universität Berlin, Berlin (Germany), 1989. Abstract available here.
  54. Manfred Schmidt-Schauß and Gert Smolka. Attributive concept descriptions with complements. Artificial Intelligence, 48(1):1-26, 1991. Available here (pdf).