The Logic ALCQI

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.

May 02 2000