Decision Procedures for Expressive Description Logics with Intersection, Composition, Converse of Roles and Role Identity

1 Introduction andMotivations

Description Logics (DLs) are a popular knowledge representation formalism based on concepts and roles, where concepts model classes of individuals, and roles model relationships between individuals [Baader et al., 2001, Chap. 1-2].

In the last years, the investigation on DLs has been driven by the modeling needs of applications ranging from semistructured data to planning [Baader et al., 2001, Part III], which have stimulated the usage of expressive constructs. For instance, to model semi-structured data one needs to represent arbitrary relations (graphs with labeled edges), and use constructs for stating irreflexivity of relations, their transitive closure, or their intersection. For reasoning about actions, one may want to express the fact that two long sequences of actions (roles) must be completed in parallel.

These applications have called for decision procedures to make reasoning services up to the modeling duties (see [Baader et al., 2001, Chap. 2] or Sec. 6). Yet, a powerful combination of constructs has so far eluded this quest: composition and intersection of roles. There is only an involved automata-based algorithm by Danecki [1984] giving a 2-EXPTIME upper bound.

∗This work was done while the author was on leave at IRIT - Toulouse partly supported by CNR grant 203-7-27. I am greatly indebted to P. Balbiani for directing my attention to logics with intersection and for countless suggestions and discussions. Discussions with F. M. Donini, I. Horrocks and U. Sattler were helpful.

Decision procedures are hard to find because DLs with intersection and composition (even without converse and role identity 1 ) haven't the tree model property. With composition and intersection, we can write concepts whose models are directed acyclic graphs. Adding role identity, we can force a relation to be well-founded or a model to be a cyclic graph.

For instance, suppose we want to model the tangled web of corporate ownerships by using the roles owns, app-board, app-CEO (denoting that a corporation owns another company, appoints the company's board of directors, or its CEO). We can represent the corporations having a doubly indirectly controlled subsidiary with the concept

corp⊓∃(app-board◦owns)⊓(owns◦app-CEO).corp

If regulators forbid corporations to be owners of themselves, we can forbid it too, without ad-hoc well-founded constructs:

∀owns⊓id(corp).⊥

We can also model, self-owned "Chinese-box" corporations:

∃(owns◦has-shares◦app-board)⊓id(corp).⊤

These models are not representable with the "classical" expressive DLs such as ALCreg or DLR.

Here, we consider the DL ALC(⊓,◦, ⊔, ·-, id(·)) which, in addition to the constructs of ALC, provides intersection, composition, union, converse of roles and role identity. ALC(⊓,◦, ⊔) is the fragment without inverse and identity.

These logics are siblings of three extensions of ALC: ALCreg with composition and transitive/reflexive closure of roles but without intersection [Baader et al., 2001, Chap.2]; ALB with intersection, union and negation [Lutz and Sattler, 2000], and possibly converse [Hustadt and Schmidt, 2001]; DLR [Calvanese et al., 1998] with intersection and role difference but only on atomic roles and with additional limitations. In the correspondence with PDL by Schild [1991], ALC(⊓,◦, ⊔) corresponds to the the *-free and test-free fragment of IPDL and ALC(⊓,◦, ⊔, ·-, id(·)) is the *-free fragment of Converse-IPDL [Harel, 1984].

In the next sections we recall some preliminaries. Then we present our tableau calculus (Sec.3), transform it into algorithms (Sec.4), sketch the complexity results (Sec.5), and discuss related works (Sec.6).

1 Role identity is the construct which, given a concept C, allows one to build a role connecting each instance of C to itself.

2 Preliminaries

Let A and P denote atomic concepts and atomic roles respectively. Concepts C, D and roles R, S are formed as follows:

A TBox T is a finite set of inclusions C ⊑D. In the sequel we focus on the satisfiability of concepts wrt empty TBoxes. However, we will build non-empty TBoxes of inclusions with a special form during the proof search itself.

An interpretation I = 〈∆I , ·I 〉 consists of a non-empty set ∆I , the domain of I - whose members are called elements - and a function ·I , the interpretation function of I, that maps every concept to a subset of ∆I and every role to a subset of ∆I ×∆I . We refer to Borgida [1996] or Baader et al. [2001, Chap. 2] for details.

An interpretation I satisfies a concept C if there exists an element d ∈ ∆I such that d ∈ CI , i.e. if CI ̸= ∅.

3 A Tableau Calculus

Taming intersection and composition requires the novel combination of a number of intuitions from the literature and some new features. They are highlighted here, for the reader familiar with the literature.

• We use the graph-based representation of rules for tableau-structures originally due to Kripke and used by Castillo et al. [1997] and Horrocks and Sattler [1999].
• We borrow the idea by Danecki [1984] of pebble games to mark elements linked by both R and S roles so that the labeling an element with both pebbles marks the intersection, triggering the insertion of suitable concepts;
• We internalize pebbles in the calculus by introducing new propositional constants as done by De Giacomo and Massacci [1997] for eventualities in CPDL.
• We use skolemization for generating "new" nodes and atomic concepts in the proof search, exploiting the results from DL translations into first-order logics [Hustadt and Schmidt, 2001].
• We exploit some semantical properties of intersection by Balbiani and Vakarelov [2001] to show we are sound.
• We use the idea of on-the fly modification of TBoxes proposed by Massacci [1998] for the universal modality.
• We borrow the idea of lazy unfolding of axioms proposed by Horrocks and Tobies [2000] for plain ALC.
• We use a new role name to denote equivalence of individuals but only for the proof search.

We use tableau-structures i.e. labeled graphs:

where N is a finite nonempty set of nodes denoted by x, y, z possibly with indices; E ⊆ N ×N is a set of oriented edges; C(·) maps nodes to sets of concepts, and R(·, ·) maps edges to sets of roles. We also use an initially empty TBox T . Inclusions of the form Ax,R⊓Ax,S ⊑ C are added on-the-fly.

Axiom: If x:A1 ∈S, x:A2 ∈S, and A1⊓A2 ⊑ C ∈ T then S ⇒ S ∪ {x:C}.

Conjunction: If x:C⊓D∈S then S ⇒S ∪ {x:C, x:D}.

Disjunction: If x:C⊔D∈S then non-deterministically either S ⇒ S ∪ {x:C} or S ⇒ S ∪ {x:D}.

Universal atomic roles: If x : ∀P.C ∈S, 〈x, y〉 : P ∈S then S ⇒ S ∪ {y:C}.

Universal role concatenation: If x:∀R◦S.C ∈S then S ⇒ S ∪ {x:∀R.∀S.C}.

Universal role intersection: If x : ∀R ⊓ S.C ∈ S then let Ax,R and Ax,S be new atomic concepts and S ⇒ S ∪ {x:∀R.Ax,R, x:∀S.Ax,S} and T ⇒ T ∪ {Ax,R⊓Ax,S ⊑ C}.

Universal role union: If x : ∀R⊔S.C ∈ S then S ⇒ S ∪ {x:∀R.C, x:∀S.C}.

Existential restriction: If x:∃R.C∈S then let y be a new node and S ⇒ S ∪ {〈x, y〉:R, y:C}.

Role concatenation: If 〈x, y〉:R◦S ∈S then let z be a new node and S ⇒ S ∪ {〈x, z〉:R, 〈z, y〉:S}.

Role intersection: If 〈x, y〉 : R⊓ S ∈ S then S ⇒ S ∪ {〈x, y〉:R, 〈x, y〉:S}.

Role union: If 〈x, y〉 : R⊔S ∈S then non-deterministically either S ⇒ S ∪ {〈x, y〉:R} or S ⇒ S ∪ {〈x, y〉:S}.

Figure 1: The reduction rules for ALC(⊓,◦, ⊔).

We start with a structure with a single node labeled with an input concept C, and apply the tableau rules to build a reduced structures without contradictions that can be used as a model for C. If none can be build, C is unsatisfiable.

The reduction rules in Fig. 1 are applicable to a tableaustructure S and a set of inclusions T for ALC(⊓,◦, ⊔). W.l.o.g. we assume that negation and converse are pushed down to atomic concepts and roles. We also abuse the DL syntax for tableau systems [Buchheit et al., 1993]: we write x : C ∈ S to indicate that C ∈ C(x), and 〈x, y〉 : R ∈ S when R ∈ R(x, y). Thus, by S ⇒ S ∪ {x:C} we mean that we obtain a new structure S ′ such that N ′ = N ∪ {x}, E ′ = E, C ′ (y) = C ′ (y) if y ̸= x and C ′ (x) = C(x) ∪ {C}, R′ (·, ·) = R(·, ·). Similarly for roles.

Most rules are close to other tableau approaches [Buchheit et al., 1993; Castilho et al., 1997; De Giacomo and Massacci, 1997; Horrocks and Sattler, 1999]. A difference is that they only label edges with atomic roles whereas we also use complex roles. So, we have rules for reducing these roles.

The role of pebbles is played by the new atoms introduced by the universal role intersection rule. The idea is that since Ax,R is new, it can label a node y only by reducing ∀R.Ax,R. thus y must be an R-successors of x. If both Ax,R and Ax,S label node y, then y is linked to x by an R⊓S role. Then we can add C to y.

Since we cannot forecast where Ax,R and Ax,S will appear, we must potentially check every node. To internalize this check into the calculus, we use the idea of on-the-fly modification of TBoxes by [Massacci, 1998]. With the intersection rule we "update" T with the inclusion Ax,R⊓Ax,S ⊑ C and then we use the Axiom rule to add C to nodes on demand.

Notice that we apply the Axiom rule only when both Ax,R and Ax,S are present in the same node. This technique, borrowed from the lazy unfolding of Horrocks and Tobies [2000], works because our inclusions are acyclic.

Notice also that the new concept Ax,R introduced by the reduction of x : ∀R⊓S.C must depend on the node where the concept is located. Following Danecki [1984, Pag. 44], one may think that it suffices to make them dependent only on the subformula (e.g. AR,∀R⊓S.C), possibly distinguishing between occurrences. This would be unsound. The concept

(∀R.∀R⊓S.C)⊓(∃(R◦R)⊓(R◦S).¬C)

is satisfiable but introducing the same "new" concepts at different nodes for the reduction of the only occurrence of ∀R⊓S.C would result in a "clash". By applying the rules of Fig. 1, one can see that the pebbles AR,∀R⊓S.C and AS,∀R⊓S.C would propagate along the "wrong" path.

The generation of new nodes and new atomic concept symbols may clearly lead to redundant rule applications or even to a non-terminating process. However, we do not need to generate really "new" nodes or atomic concepts. We can use the equivalent of skolemization (or Hilbert's ϵ-terms) introduced by Ohlbach and later refined by Hustadt and Schmidt [2001] for the translations of DLs into first-order logic.

The generation of skolem functions is standard and we assume that for "new" concepts we use the function GENCONCEPT(x,R), and for "new" nodes we use GENNODECONCEPT(x,C) and GENNODEROLE(x, y,R). So, when reducing x:∃R.C, we call y = GENNODECONCEPT(x, ∃R.C) and add y :C and 〈x, y〉:R to the structure.

Definition 1 A tableau structure S and a set of inclusions T are reduced for a rule R if the application of R maps S and T into themselves. A structure and a set of inclusions are reduced if they are reduced for all rules.

Definition 2 A tableau-structure contains a clash if there is a node x and a concept C such that {C, ¬C} ⊆ C(x).

Theorem 1 A concept C of ALC(⊓,◦, ⊔) is satisfiable iff there is a non-deterministic application of the rules in Fig. 1 to an initially empty TBox and a structure with only one node labeled with C leading to a reduced and clash-free structure.

For every feature, the proof cleverly combines the techniques from the cited works in the literature. The twist is the soundness of the universal role intersection rule. To this extent, we set AIx,R = {y| 〈x, y〉 ∈ RI } and similarly for S. In words, the newly introduced concepts are fulfilled by the appropriate individuals R-reachable, or S-reachable, from x. Due to lack of space, details are left to the full paper.

Next, we define the tableau rules for the full language. Beside converse, the tricky bit is the presence of the intersection between role identity and complex roles: id(C)⊓R is a selfloop describing individuals in the class C that are in relation R with themselves (e.g. the self-owned companies). To this extent we employ an atomic role symbol (not occurring in the input concept) for equality of nodes ·≈·.

Universal converse of roles: If y :∀R-.C ∈S, 〈x, y〉 :R ∈S then S ⇒ S ∪ {x:C}.

Universal role identity: If x : ∀id(D).C ∈S then S ⇒ S ∪ {x:¬D⊔C}.

Role converse: If 〈x, y〉:R- ∈S then S ⇒S ∪ {〈y, x〉:R} .

Role identity: If 〈x, y〉:id(C)∈S then S ⇒S ∪ {x≈y, x:C} Role identity distribution: If x≈y ∈ S and x : C ∈S then S ⇒ S ∪ {y:C}. Role identity symmetry: If x≈y ∈ S then S ⇒S ∪ {y≈x}.

Role identity transitivity: If x≈y ∈ S and y≈z ∈ S for then S ⇒ S ∪ {x≈z}.

Algorithm WORLDS; input node x0 ; set of concepts C; set of inclusions T ; output sat if C is satisfiable, unsat otherwise; variables node x; labeled graph S; beginN= {x0 }; E= ∅; C(·)= {〈x0 , C〉}; R(·, ·) = ∅; if CLASH(S) then return(unsat); while x=CHOOSENODE(S,T )=/=none do R=CHOOSERULE(x,S,T ); "Apply R to x, S, T updating S and T " if CLASH(S) then return(unsat); forall x ∈ N \ {x0 } do if WORLDS(x,C(x),T )==unsat then return(unsat ); return sat

end;

Figure 3: The algorithm for ALC(⊓,◦, ⊔)

The reduction rules in Figure 1 and the additional rules in Figure 2 are applicable to a tableau-structure S and a set of inclusions T for the logic ALC(⊓,◦, ⊔, ·-, id(·)).

The rules for ·≈· might be eliminated if the rule for id(·) collapses nodes. However, this would complicate the algorithms, as we would need a unique way for collapsing nodes.

Theorem 2 A concept C of ALC(⊓,◦, ⊔, ·-, id(·)) is satisfiable iff there is a non-det. application of the rules in Fig. 1,2 to an initially empty TBox and a structure with only one node labeled with C yielding a reduced and clash-free structure.

4 FromCalculi to Algorithms

The PSPACE-algorithm for ALC(⊓,◦, ⊔) is called WORLDS after Ladner's WORLD for modal logic K. It is plural because each call works on a fragment of a Kripke model and not just on a set of concepts true for an individual. It is in Fig. 3.

To check the satisfiability of a concept C one calls WORLDS(0,{C},∅) and applies the rules from Fig. 1.

In the algorithms, we use the symbol "=" for assignment, and "==" for equality testing. We assume all functionalities for working with labeled direct graphs, an auxiliary function CLASH(S) which detects clashes, and auxiliary procedures for selecting objects: CHOOSENODE selects a node to be reduced; CHOOSERULE selects an applicable rule for a node.

Algorithm CWORLDS; input node x0 ; set of concepts C; output set of concepts D⊃C if C is satisfiable, unsat otherwise; variables node x; S labeled graph; D set of concepts; global variables set of inclusions T ; beginN= {x0 }; E= ∅; C(·)= {〈x0 , C〉}; R(·, ·) = ∅; if CLASH(S) then return unsat ; start: while x=CHOOSENODE(S,T )=/=none do R=CHOOSERULE(x,S,T ) "Apply R to x, S and T updating S and T " if CLASH(S) then return unsat ; forall x ∈ N \ {x0 } do D=CWORLDS(x,C(x)); if D==unsat then return unsat; else if C(x)=/= D; then C(x)= D; goto start; return(C(x0 )) end;

These procedures must work in time polynomial in the size of the input and respect the following constraints:

Search Criteria 1 A rule is not selected if the structure is already reduced for it. A node is not selected if the structure is already reduced for all rules applicable to the node.

Search Criteria 2 The Existential restriction rule is selected only for reduction of concepts labeling the initial node x0 .

If the procedures cannot select anything respecting the above constraints they return the value none.

The tricky bit is showing that the algorithm is in PSPACE (Sec. 5). We just highlight the differences from trace-based methods used for ALC by Ladner [1977], Schmidt-Schauss and Smolka [1991] or Tobies [2001].

The classical tableau-based algorithm for ALC would have been identical to ours except for the last for cycle:

for all ∃R.C ∈ C(x0 ) do if WORLD({C} ∪ {D | ∀R.D ∈ C(x0 )})==unsat then return(unsat )

In words, for ALC we explore the one-step R-successors of x0 by recursively calling the procedure. So, we only examine one node (x0 ) at every call.

The WORLDS algorithm examines the initial node x0 and reduces all existential concepts labeling x0 , i.e. all one step R-successors of x0 . Thus, it builds a fragment of the Kripke structure. However, the reduction of existential-concepts labeling successors nodes is deferred to recursive calls. The rules for intersection and composition may transform a "onestep" R-successors into "many-steps" atomic P-successors. Still, the number of intermediate P-steps is linearly bounded by the size of the input concept.

The full algorithm is called CWORLDS because it returns a set of concepts. It is shown on Figure 4. The rules that can be applied to the algorithm are those from Fig. 1,2. It must respect an additional search constraint:

Search Criteria 3 If x1 ≈ x2, x2 ≈ x3,. . . xn-1 ≈ xn are present in the structure then only one node xi ∈ {x1, . . . xn} can be selected for the recursive call of CWORLDS in the forall cycle. If x0 is among them, none can be selected.

We must return a set of concepts rather than just sat to cope with converse and role identity. The idea is borrowed from modal logics with symmetric relations [Massacci, 2000] and DLs with converse [Tobies, 2001].

For example, the concept ∃R◦id(∃id(∀R.C).⊤)◦R.¬C is unsatisfiable. If we used algorithmWORLDS with the full set of rules it would return sat. The explanation is that we would introduce a node y labeled by ∃id(∀R.C).⊤ and would evaluate the existential concept in the next recursive call. In the recursive call we would add ∀R.C to the initial node (which would correspond to y) but we could not use this information to derive a clash in the initial call.

The use of skolemization, rather than truly fresh names, is necessary to guarantee that CWORLDS is both correct and terminating. For instance, if fresh names are used in the recursive calls following a restart, the concept ∃R.∃S.∀S- ⊓T.C would make CWORLDS non-terminating.

5 Complexity Analysis

We denote by n the size of the input concept C which must be proved (un)satisfiable, measured as the number of symbols.

We first prove that WORLDS requires only polynomial space in n. The idea is that ALC(⊓,◦, ⊔) lost the tree-model property but kept the cactus-model property.

Loosely speaking, our models can be arranged into the shape of a cactus, i.e. a tree in which the edge connecting two nodes of the tree is not a slim branch but a "fat", cactus-like stem. This fat stem is made by other nodes and edges, but its size is polynomially bounded by n. Many stems sprout from each stem, as in a real cactus, but their number is still polynomially bounded. Since the height of the cactus is also polynomially bounded we are done.

Concepts labeling nodes can be seen as spikes. We must also prove that they aren't exponentially many. For most DLs this is obvious: we only introduce subconcepts of the input concept. Here, we introduce new atomic concepts.

The next tree lemmata make these intuitions precise. At first, we say that the cactus height is polynomially bounded:

Lemma 1 The call stack of WORLDS is at most O(n) deep.

Then the size of each cactus stem is bounded:

Lemma 2 Each invocation of WORLDS generate a structure with at most O(n) nodes.

Finally, we say that the the number of spikes is bounded.

Lemma 3 The number of new atoms occurring as (sub)concepts in the the labels of the nodes of an invocation of WORLDS is bounded by O(n3 ).

To prove Lemma 1 we cannot use the standard proof that each interaction reduces the modal depth (nesting of universal and existential roles) of the set of concepts labeling a node because of the Axiom rule. We need a new notion of modal depth: we associate different depths to atomic concepts from the input concept and to "invented" atomic concepts.

• if A is from input concept then d(A) = 0
• if Ax,R is an atomic concept introduced by the reduction of one or more x : ∀R⊓S.C then d(Ax,R) is equal to maxS,C{d(C)|x:∀R⊓S.C}
• d(∀R.C) = |R|+d(C) where |R| is the size of R, measured as the number of symbols.

Now by induction on the number of applied rules we can show that for all nodes x ̸= x0 and all concepts C ∈ C(x), there is a concept D ∈ C(x0 ) such d(D) > d(C). Since the depth of every concept, and hence the maximal depth of a set of concepts, is bounded by n we are done.

For the proof of Lemma 2, observe that new nodes in the structure S can only be created by two rules: the rules reducing existential and the rules reducing composition of roles. The first rule can only be applied to x0 , thus bounding the nodes so introduced by O(n). For the second rule, the number of nodes thus introduced is bounded by O(n).

For Lemma 3, observe that two "new" concepts are introduced only when we reduce an universally quantified role intersection. The newly generated concepts depend on the same node and on the roles which are immediate subroles of an intersection of roles occurring in the input concept. Hence, by Lemma 2, for each invocation we can create at most O(n · n) different new concepts. By Lemma 1 the number of nested recursive calls of WORLDS is at most O(n). When a leaf call is reached we generated at most O(n2 · n) different concepts.

Theorem 3 WORLDS can be implemented using only polynomial space in n.

For the proof observe that the stack is at most O(n) deep by Lemma 1 and for each call of WORLDS at depth i we have

• O(n) + O(n) new nodes and at most O(n2 ) edges,
• O(n4 ) concepts for each node and each concepts taking at most O(n) space,
• O(n) roles labeling each edge and each role taking at most O(n) space
• O(i · n5 ) inclusions, which can be added by reducing a concept x : ∀R⊓S.C where the number of different xs is bounded by Lemma 2, R⊓S occurs in the input concept and C either occurs in the input concept or is one of O(n3 ) new concepts invented at any j ≤ i steps.

PSPACE-hardness follows fromALC.

Corollary 4 The satisfiability of ALC(⊓,◦, ⊔) concepts is PSPACE-complete.

The NEXPTIME-upper bound of ALC(⊓,◦, ⊔, ·-, id(·)) satisfiability, has a more involved proof. The analogous of Lemma 1 and Lemma 2 can be proved with a similar argument. The only twist is observing that, by Criteria 3, we only reduce the existential concepts in one of the node linked by the equality predicate. Thus, we never recursively call CWORLDS on the nodes "equal" to the root node x0 (as for them the induction would fail). The equivalent of Lemma 3 fails and we only have a global bound:

Lemma 4 The total number of new atoms occurring as (sub)concepts in the the labels of the nodes throughout the execution of WORLDS is bounded by O(nn ) = 2O(n log n) .

Using Lemma 4, we bound the number of concepts labeling a formula to O(n) · 2O(n log n) = 2O(n log n) and the number of inclusions by doubling the multiplicative constant in the O(n log n) expression at the exponent.

Theorem 5 CWORLDS terminates after 2O(n2 logn) time.

For the proof observe that CWORLDS can be "restarted" at most finitely many times. More precisely, (i) the set of concepts returned by CWORLDS is larger or equal to the initial set upon which CWORLDS is called (in symbols C(x0 ) ⊇ C), and (ii) the total number of concepts is bounded by 2O(n logn) . Then the total number of restarts for a structure in a single invocation of CWORLDS is bounded by O(n) · 2O(2n log n) . The bound on the stack does the rest.

Corollary 6 The satisfiability of ALC(⊓,◦, ⊔, ·-, id(·)) concepts is in NEXPTIME.

An intriguing question is why the standard technique for giving PSPACE-bounds for DLs with converse [Tobies, 2001] or symmetric modal logics [Massacci, 2000] fails here. According this technique, we take the "converse-free" algorithm and add some "restarts" (this is what CWORLDS does). For the bound, we observe that (i) restarts add a bounded number of new concepts (indeed subconcepts of the input concept) and (ii) the time wasted by restarts doesn't matter.

The argument fails here because converse or role identity and intersection plus composition can force CWORLDS to label a node with exponentially many new atomic concepts.

To force this exponential generation of concepts, we start by constructing a concept Gn whose model is a cyclic graph with edges labeled by two roles R and S. Looking only at role R, the graph is a binary tree with height n, with Gn labeling its root. Each S-edge connects the child node of an R-edge to its parent. The key feature of Gn is that we can start at the root, traverse forward a path of R-edges, reach a leaf and then continue to traverse S-edges forward to the root. Once there, we can take another R-path, and so on. The model of Gn has a path whose length is exponential in n. Pictorially, Gn can be seen as a daisy with exponentially many petals.

This construction is impossible in ALC, ALC with converse, or ALC(⊓,◦, ⊔) because there are always acyclic models. In ALC we can keep on traversing edges (roles) on one path until we arrive at dead-end. Since the depth of the longest path is linear in the size of the concept to be verified we are done. In ALC with converse, edges can be oriented forward or backward: we get a two-ways path but still it terminates into a dead-end. With intersection we must check that two paths meet at certain points but the idea is the same.

Still, CWORLDS only uses polynomial space for visiting Gn. The problems start when we add to Gn one or more concepts that ask to verify the intersection of two paths. Loosely speaking, one path reaches the top of a petal, the other goes back to center, then round another petal and back to the top of the first petal. The problem is that we don't know a priori which petal we must visit among the exponentially many that are available. We can put one of these concepts in each leaf. Then, the number of pebbles that accumulate in the root, restart after restart, will be exponential in n.

6 RelatedMethods

A number of decision procedures and complexity results for logics extending ALC (or multimodal K) can be found in the literature. Yet, none of them fully tackle our results.

With respect to complexity results based on encodings, De Giacomo and Lenzerini [1995] proved the EXPTIMEcompleteness of a DL with composition, converse and intersection restricted to atomic roles with additional limitations. Calvanese et al. [1998] proved the EXPTIME-completeness of DLR, where intersection, union and difference of roles are allowed but composition is not permitted. Baader and Sattler [1999] proved the undecidability of a number of combination of expressive DLs with number restrictions and intersection.

With respect to decision procedures, Horrocks et al. [1999; 2000] tamed expressive DLs with converse and rolehierarchies where intersection between atomic roles can be simulated. They do not allow for composition of roles. Baader and Sattler [1999] have proposed an EXPTIMEcalculi for ALC with number restrictions with composition, intersection and union of role chains. However, concepts are restricted to plain ALC. Lutz and Sattler [2000] give a decision procedure for ALB (ALC plus intersection, union, and negation of roles but without composition). Tobies [2001] gives a PSPACE-algorithm for DLs with number restrictions, converse and intersection of atomic relations.

In the realm of modal and dynamic logic, Danecki [1984] has shown, using automata-based techniques, that IPDL (PDLwith Intersection) can be decided in 2-EXPTIME. IPDL strictly extends the logic ALC(⊓,◦, ⊔) allowing for the transitive and reflexive closure of roles and for role identity. However, Danecki claims that it is possible to use pebbles which depends only on the occurrence of the subformula. For our calculus, this is unsound and Danecki's involved construction may need to be checked against our counterexample. For Converse-PDL automata theoretic techniques have been proposed by Vardi and Wolper [1986] and a tableau calculus has been given by De Giacomo and Massacci [1997].

Hustadt and Schmidt [2001] have shown a decision procedures for boolean modal logic with converse. Their procedure is based on a clever translation into first-order logic of modal formulae followed by a decision procedure for the guarded fragment. They only prove decidability results. The possibility of a PSPACE-algorithm for the extension of ALC with intersection, converse and union is just claimed.

Decision procedures for first order logic with two variables (see the survey by Gr¨ adel and Otto [1999]) can be used for DLs with intersection but without composition, via first-order translations. One could also use the decision procedures by Ganzinger and De Nivelle [1999] for the guarded fragment. Current methods based on translations into decidable fragments of first order logic cannot treat intersection and composition at the same time, as this requires to have at least three variables and does not allows for guards in predicate clauses.