Franz Baader and Ulrike Sattler
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.