Introduction

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:

$$\texttt{Human}\sqcap (\texttt{Male}\sqcup \texttt{Female} ) \... ...xttt{Female} )}\sqcap \forall \texttt{hasChild} .\texttt{Human}$$

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 hasChild), instead of allowing only for existential or universal restrictions like . is a syntactic variant of the (multi-)modal logic $\mathsf{K}$ with graded modalities [Fin72]. In this paper we will study problems for the DLs and . The latter extends with the possibility to refer to the inverse of role relations. Additionally, in this paper we will encounter nominals, i.e., concepts referring to single elements of the domain. The extensions of and with nominals are denoted by and . An example concept of that describes the common children of the individuals ALICE and BOB living with ALICE or BOB is

$$\exists {\texttt{hasChild} ^{-1}}.{\texttt{ALICE} } \sqcap \e... ...s {\texttt{livesWith} }.(\texttt{ALICE}\sqcup \texttt{BOB} ) .$$

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

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.

$$\begin{align*}\texttt{Parent} & = \texttt{Human}\sqcap (\geqslant 1 \; {\texttt... ... \ensuremath{(\geqslant 2 \; \texttt{hasChild}\; \texttt{Toddler} )}\end{align*}$$

The next expressions are general axioms stating that males and females are disjoint ($\bot$ denotes the empty concept) and that males or females coincide with those humans having exactly two human parents.

$$\begin{align*}\texttt{Female}\sqcap \texttt{Male} & = \bot\\ \texttt{Female}\s... ...{Human}\sqcap (= 2 \ \texttt{hasChild} ^{-1} \ {\texttt{Human} }) \end{align*}$$

Finally, the following expression is a cardinality restriction expressing that there are at most two earliest ancestors:

$$(\leq 2 \; (\texttt{Human}\sqcap \ensuremath{(\leqslant 0 \; \texttt{hasChild} ^{-1} \; \texttt{Human} )} ))$$

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).

  

Figure 1: Complexity results established in this paper (shown in bold face)

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] ¹ , 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].