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:
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.
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].