Reasoning with Nominals

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 *

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

May 02 2000