Next: Expressing Cardinality Restrictions Using Up: The Complexity of Reasoning Previous: Reducing Domino Problems to

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

Definition 4.1   Let NI be a set of individual names (also called nominals) disjoint from NC and NR. Concepts in are defined as -concepts with the additional rule that, for every , o is an -concept. A general concept inclusion axiom for is an expression of the from , where C and D are -concepts. A for is a finite set of general inclusion axioms for , where the subscript I'' stands for Inclusion''. The semantics of concepts is defined similar as for , with the additional requirement that every interpretation maps a nominal to a singleton set ; o can be seen as a name for the element in . Please note that we do not have a unique name assumption, i.e., we do not assume that implies .

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.

Lemma 4.2
Consistency of or both for and is -hard and can be decided in , if unary coding of numbers is used.

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.

Next: Expressing Cardinality Restrictions Using Up: The Complexity of Reasoning Previous: Reducing Domino Problems to

Stephan Tobies
May 02 2000