Next: Consistency of - is Up: The Complexity of Reasoning Previous: Introduction

# The Logic ALCQI

Definition 2.1   Let NC be a set of atomic concept names and NR be a set of atomic role names. Concepts in are built inductively from these using the following rules: all are concepts, and, if C, C1, and C2 are concepts, then also

are concepts, where and S=R or S= R-1 for some . A cardinality restriction of is an expression of the form or where C is a concept and ; an - 2 is a finite set of cardinality restrictions. The semantics of concepts is defined relative to an interpretation , which consists of a domain and a valuation that maps each concept name A to a subset of and each role name R to a subset of . This valuation is inductively extended to arbitrary concepts using the following rules, where denotes the cardinality of a set M:

An interpretation satisfies a cardinality restriction iff , and it satisfies iff . It satisfies a T iff it satisfies all cardinality restrictions in T; in this case, is called a model of T and we will denote this fact by . A that has a model is called consistent. With we denote the fragment of that does not contain any inverse roles R-1.

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:

Lemma 2.2
Consistency of an - T can be decided in .

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.

Next: Consistency of - is Up: The Complexity of Reasoning Previous: Introduction

Stephan Tobies
May 02 2000