Nominals, i.e., atomic concepts referring to single individuals of the domain, are studied both in the area of DLs [BPS94,DLNS96] and modal logics [GG93,BS96,ABM99]. In this section we show how, in the presence of nominals, consistency for can be polynomially reduced to consistency of TBoxes consisting of general inclusion axioms, which, in general, is an easier problem. This correspondence is used to obtain two novel results: (i) we show that, for unary coding, consistency of -TBoxes consisting of cardinality restrictions can be decided in ; (ii) we show that, in the presence of both inverse roles and number restrictions, reasoning with nominals is strictly harder than without nominals: the complexity of determining consistency of TBoxes with general axioms rises from to , and the complexity of concept satisfiability rises from to .
An interpretation satisfies an axiom iff . It satisfies a iff it satisfies all axioms in ; in this case is called a model of , and we will denote this fact by . A that has a model is called consistent.
Cardinality restrictions, , and their interpretation for are defined analogously to .
With we denote the fragment of that does not contain any inverse roles R-1.
Proof. Consistency of (and hence of ) is -hard already for (a syntactical variant of) [HM92]. Assuming unary coding of numbers, we can reduce the problems to satisfiability of , which yields the upper bound.