Description Logics: Basics, Inference Algorithms, and Applications

IJCAR 2001 Tutorial

Ian Horrocks - Ulrike Sattler

Goal and content of the tutorial

This tutorial is targeted towards participants with a basic background in Computer Science or Logic, and provides them with the basic principles of knowledge representation based on Description Logics (DLs). DLs are a family of knowledge representation formalisms designed for the representation of and reasoning about terminological knowledge, which are offsprings of semantic networks and frame-based systems. Interestingly, DLs are also closely related to Modal and Dynamic Logics. In recent years, it has turned out that DLs are also well-suited to the representation of and reasoning about database conceptual models, information integration, and ontologies. A variety of different DLs exist, with different expressive power and different computational complexity of the corresponding inference problems. Tableaux-based algorithms deciding these problems for expressive DLs (i.e., with PSpace- and ExpTime-complete inference problems) have proved to be be amenable to optimisation, and to behave well even for very expressive DLs (i.e., with ExpTime-complete inference problems). Based on implementations of these algorithms, other tools are being developed to be used in the above mentioned applications of DLs.

Starting from the historical perspective, we will introduce a basic DL, ALC (a well-known DL closely related to the Modal logic K), the corresponding inference problems subsumption and satisfiability, and describe a reasoning algorithm based on tableaux. We will sketch how this basic algorithm can be modified to deal with other DL constructors such as transitive roles, inverse roles, number restrictions, and general concept inclusion axioms. Finally, we will present two example applications of DLs together with DL-based tools for these applications, namely the tool OilEd for the design and evolution of ontologies and for the design of (integrated) conceptual models. Depending on the time left and the interest of the participants, we will also mention implementation and optimisation techniques for DL reasoners.

This tutorial will provide the participants with a general understanding of what DLs are and their history, the current state-of-the-art, a rough understanding of reasoning techniques employed for expressive DLs, and an insight into applications of DLs.

Prerequisite knowledge

The tutorial requires only a basic background knowledge in Computer Science or Logic (i.e., propositional logic will suffice, but predicate logic will help), and does not require any specific background knowledge in logic.


 Name: Ian Horrocks Ulrike Sattler
 Address: Department of Computer Science    LuFG Theoretische Informatik
   University of Manchester RWTH Aachen
   Oxford Road Ahornstr. 55
   Manchester, M13 9PL, UK 52074 Aachen, Germany
 Phone: (+44 161) 275 6133 (+49 241) 80 21140
 Fax: (+44 161) 275 6932 (+49 241) 88 88 360


F. Baader and U. Sattler.
Tableau algorithms for description logics.
In R. Dyckhoff, editor, Proc. TABLEAUX 2000, volume 1847 of LNAI, pages 1-18, St Andrews, Scotland, UK, 2000. Springer-Verlag.

I. Horrocks.
Using an Expressive Description Logic: FaCT or Fiction?
In Proc. of KR-98, 1998.

I. Horrocks, U. Sattler, and S. Tobies.
Practical reasoning for expressive description logics.
In H. Ganzinger, D. McAllester, and A. Voronkov, editors, Proc. of LPAR'99, number 1705 in LNAI, pages 161-180. Springer-Verlag, 1999.