Description Logics (DLs) can be used in knowledge based systems to represent
and reason about taxonomical knowledge of the application domain in a semantically
well-defined manner [WS92].
They allow the definition of complex concepts (i.e., classes, unary
predicates) and roles (binary predicates) to be built from atomic ones by the
application of a given set of constructors. For example, the following concept
describes those parents having at least two daughters:

This concept is an example for the DL . extends the ``standard'' DL [SSS91] by qualifying number restrictions, i.e., concepts restricting the number of individuals that are related via a given role (here

Here, the parent relationship is expressed as the inverse of the

A terminological component (TBox) allows for the organisation of defined concepts and roles and forms the knowledge base of a DL system. TBoxes studied in DLs range from weak ones allowing only for the acyclic introduction of abbreviations for complex concepts, over TBoxes capable of expressing various forms of general axioms, to cardinality restrictions that can express restrictions on the number of elements the extension of a concept may have. In the following, we give examples of these three types of assertions.

The following TBox introduces parent as an abbreviation for a human having at least one child and whose children are all human, toddler for very young human, and busy parent for a parent having at least two children that are toddlers.

Cardinality restriction were first introduced in [BBH96] as a terminological formalism for the DL ; as we will see, they can express general axioms and hence are the most expressive of the terminological formalisms considered in this paper.

A key component of a DL system is a reasoning component that provides services
like subsumption or consistency tests for the knowledge stored in the TBox. A
subsumption test, for example, could infer from the previous definitions that
both
`Male` and
`Female` are subsumed by
`Human` and that
`BusyParent` is subsumed by
`Parent` as each busy parent must
have at least one child. There exist sound and complete algorithms for
reasoning in a large number of DLs and different TBox formalisms that are
optimal with respect to the known worst-case complexity of these problems
(see [DLNS96] for an overview).

In this paper we establish a number of new complexity results for DLs with cardinality restrictions or nominals. Figure 1 summarises the new complexity bounds established in this paper. All problems are complete for their respective complexity class. This paper is organised as follows.

After giving some basic definitions in Section 2, we show
that consistency of TBoxes with cardinality restrictions for
is a
-complete problem (Section 3). Membership in
is shown by a translation
to the satisfiability problem of
[PST97]
^{1}
, the two variable fragment
of first order predicate logic augmented with counting quantifiers. The
matching lower bound is established by a reduction from a
-complete
bounded domino problem.

In Section 4, we show that reasoning with cardinality
restrictions can be reduced to reasoning with the (weaker) formalism of
general axioms in the presence of nominals. This yields interesting complexity
results both for reasoning with cardinality restrictions and with nominals.
Using a result from [De 95], the reduction shows that consistency
of TBoxes with cardinality restrictions for
is in
.
This
improves the result from [BBH96], where it was shown that the problem
can be solved in
.
Moreover, we show that for a DL with number
restrictions, inverse roles, and nominals reasoning problems become
-hard, which solves an open problem from [De 95]. This
combination is of particular interest for the application of DLs in the area
of reasoning with database
schemata [CDL^{+}98,CDGL98a].

May 02 2000