Using the constructors from Definition 2.1, we use
as an abbreviation for the cardinality restriction
and introduce the following abbreviations for concepts:
TBoxes consisting of cardinality restrictions have first been studied in [BBH96] for the DL . Obviously, two concepts C,D have the same extension in an interpretation iff satisfies the cardinality restriction . Hence, cardinality restrictions can express terminological axioms of the form C = D, which are satisfied by an interpretation iff . General axioms are the most expressive TBox formalisms usually studied in the DL context [DL96]. One standard inference service for DL systems is satisfiability of a concept C with respect to a T, i.e., is there an interpretation such that and . For a TBox formalism based on cardinality restrictions this is easily reduced to TBox consistency, because obviously C is satisfiable with respect to T iff is a consistent . For this the reason, we will restrict our attention to consistency; other standard inferences such as concept subsumption can be reduced to consistency as well.
Until now there does not exist a direct decision procedure for consistency. Nevertheless this problem can be decided with the help of a well-known translation of - to [Bor96], given in Figure 2. The logic is the fragment of predicate logic in which formulae may contain at most two variables, but which is enriched with counting quantifiers of the form . The translation yields a satisfiable sentence of if and only if the translated is consistent. Since the translation from to can be performed in linear time, the upper bound [GOR97,PST97] for satisfiability of directly carries over to - consistency:
Please note that the -completeness result from [PST97] is only valid if we assume unary coding of numbers in the input; this implies that a number n may not be stored in logarithmic space in some k-ary representation but consumes n units of storage. This is the standard assumption made by most results concerning the complexity of DLs. We will come back to this issue in Section 3.3.