PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 95 (109) (2014), 133–147 DOI: 10.2298/PIM1409133M

ON THE COMPLEXITY OF (RESTRICTED) ALCIr

Milenko Mosurović and Michael Zakharyaschev

Communicated by Žarko Mijajlović

Abstract. We consider a new description logic ALCI r that extends ALCI with role inclusion axioms of the form R ⊑ QR_{1} … R_{m} satisfying a certain regularity condition. We prove that concept satisfiability with respect to RBoxes in this logic is ExpTime-hard. We then define a restriction ALCI r^{−} of ALCI r and show that concept satisfiability with respect to RBoxes in ALCI r^{−} is PSpace-complete.

1. Introduction

Description logics (DLs, for short) are well-known knowledge representation formalisms in AI [2] and the Semantic Web, underlining the Web Ontology Language OWL 2.^{1} The language of DLs is built around concept names (unary predicates) and role names (binary predicates) using various constructs such as the Booleans, universal and existential restrictions, taking the inverse of a role, etc. The resulting complex concepts and roles are used to form knowledge base (or ontology) axioms. For example, the axiom Parent ≡ Person ⊓ ∃hasChild. Person defines a parent as a person who has child, which is also a person, while ancestor ∘ ancestor ⊑ ancestor says that ancestor is a transitive role. An important feature of standard DLs is that reasoning problems such as concept and role satisfiability with respect to knowledge bases or instance checking are decidable and reasonably scalable in practice; moreover, there are a number of highly optimized DL reasoners for performing those reasoning tasks.^{2}

In recent years, a considerable interest has been attracted to DLs with complex role inclusion axioms of the form R_{1} ∘ ⋯∘ R_{n} ⊑ S_{1} ∘ ⋯∘ S_{k}, where the R_{i} and S_{j} are role names or their inverses. Such axioms are required, for instance, in multiple use cases in the life sciences domain and ontological product modelling and collaborative design [14, 5, 3, 12]. In fact, complex role inclusion axioms were already used in the original KL-ONE terminological language [4], where they were called ‘role-value-maps’ and could be applied to certain individuals. However, it turned out [16] that KL-ONE was undecidable. One way to defeat undecidability is to restrict the right-hand side of role inclusions to a single role and impose on them a certain regularity condition, which is done in the DL SROIQ underlying OWL 2 [9, 5] (see also [1, 7, 10, 8, 11]).

2010 Mathematics Subject Classification: 68T27, 03B70, 68T30, 68W40, 68Q25.

1http://www.w3.org/TR/owl2-overview/

2See, e.g., http://en.wikipedia.org/wiki/Description_logic#Tools

A decidable DL, SR^{+} OIQ , with role inclusion axioms that allow a non-trivial right-hand side (and also satisfy a regularity condition) has been recently constructed in [13]. However, the exact complexity of reasoning with this logic is still unknown. To understand the impact of such role inclusions, we here consider the fragment ALCIr of SR^{+} OIQ which extends the basic DL ALCI with axioms of the form R ⊑ QR_{1} …R_{m} satisfying the same regularity condition as SR^{+} OIQ . We prove, in Section 3, that concept satisfiability with respect to RBoxes (finite sets of role inclusion axioms) in ALCIr is ExpTime-hard. However, we have not managed yet to obtain a matching upper bound. Instead, in Section 4, we develop a PSpace tableau-based decision algorithm for a fragment of ALCIr which imposes further restrictions on role inclusion axioms.

2. Description Logic ALCIr

We begin by formally defining the syntax and semantics of the description logic ALCIr. The alphabet of ALCIr consists of two countably infinite and disjoint sets N_{C} and N_{R} of concept names and role names, respectively. This alphabet is interpreted in structures, or interpretations, of the form I = (Δ^{I} , ·^{I} ), where Δ^{I} ≠ ∅ is the domain of interpretation and ·^{I} an interpretation function that assigns to every A ∈ N_{C} a subset A^{I} ⊆ Δ^{I} and to every R ∈ N_{R} a binary relation R^{I} ⊆ Δ^{I} × Δ^{I} .

We now introduce the role and concept constructs that are available in ALCIr, together with their interpretations. For each role name R ∈ N_{R}, the inverse R^{−} of R is interpreted by the relation

(R^{−} )^{I} = {(y, x) ∈ Δ^{I} × Δ^{I} | (x, y) ∈ R^{I} }.

We call role names and their inverses basic roles, set N_{R}^{−} = N_{R} ∪ {R^{−} | R ∈ N_{R}} and write rn(R) = rn(R^{−} ) = R, for R ∈ N_{R}. We define an ALCIr-role as a chain R_{1} …R_{n} of basic roles R_{i} and interpret it by taking

(R_{1} …R_{n})^{I} = R_{1}^{I} ∘ ⋯∘ R_{n}^{I},

where ∘ denotes the composition of binary relations. We also define a function inv(·) on role chains by inv(R_{1} ⋯ R_{n}) = inv(R_{n}) ⋯ inv(R_{1}), where inv(R) = R^{−} and inv(R^{−} ) = R, for R ∈ N_{R}.

ALCIr-concepts, C, are defined by the following grammar, where A ∈ N_{C} and R is a basic role:

C ::= A | ⊥ | ⊤ | ¬C | C_{1} ⊓ C_{2} | C_{1} ⊔ C_{2} | ∃R.C | ∀R.C.

The interpretation of these concepts is defined as follows:

⊤^{I} = Δ^{I} ,  ⊥^{I} = ∅,  (¬C)^{I} = Δ^{I} ∖ C^{I} ,
(C_{1} ⊓ C_{2})^{I} = C_{1}^{I} ∩ C_{2}^{I} , (C_{1} ⊔ C_{2})^{I} = C_{1}^{I} ∪ C_{2}^{I} ,

ON THE COMPLEXITY OF (RESTRICTED) ALCI r 135

(∃R.C)^{I} = {x ∈ Δ^{I} | ∃y ∈ C^{I} (x, y) ∈ R^{I} },

(∀R.C)^{I} = {x ∈ Δ^{I} | ∀y ((x, y) ∈ R^{I} → y ∈ C^{I} )}.

An RBox, R, is a finite set of role inclusions axiom (RIs) of the form

R ⊑ QR_{1} …R_{m}, m ⩾ 1,

where R, Q, R_{1}, …, R_{m} are basic roles satisfying the following regularity condition: the transitive closure of the relation induced by rn(R) ≺ rn(Q), for all such RIs in R, is a strict partial order on the set of role names. We denote this strict partial order by ≺_{R}. If ϱ_{i} is a role, i = 1, 2, then ϱ_{1} ⊑ ϱ_{2} is satisfied in I if ϱ_{1}^{I} ⊆ ϱ_{2}^{I}. We say that an RBox R is satisfiable if there exists an interpretation I satisfying all the members of R. In this case we write I ⊧ R and call I a model of R.

The main reasoning problem we are concerned with in this paper is concept satisfiability with respect to an RBox: given an ALCIr concept C and an RBox R, decide whether there is a model I of R such that C^{I} ≠ ∅.

For a concept C, we denote by role(C) the set of all basic roles R such that at least one of R or inv(R) occurs in C; role(C, R) contains those basic roles and their inverses that occur in C or R.

We assume that all concepts are in negation normal form (NNF). In particular, when we write ¬C, for a concept C, we actually mean the NNF of ¬C. Denote by con(C) the smallest set that contains C and is closed under sub-concepts and ¬.

The DL ALCIr defined above is an extension of the well-known DL ALCI [2] with regular RBoxes. Thus, concept satisfiability w.r.t. RBoxes in ALCIr is PSpace-hard. On the other hand, ALCIr is a fragment of the decidable DL SR^{+} OIQ [13] the precise complexity of reasoning in which is still unknown.

3. ExpTime-Hardness

In this section we establish an ExpTime lower bound for the complexity of concept satisfiability w.r.t. RBoxes in ALCIr. The following example illustrates the reduction used in the proof.

Example 3.1. Let R = {R ⊑ QR}. Consider the concept

C_{0} = (¬A_{n−1} ⊓ ⋯⊓ ¬A_{0}) ⊓ ∃R.⊤ ⊓ C′⊓ C′′,

where

C′ = ⨅_{k=0}^{n−1} ∀R.∀R^{−} .( ( ⨅_{i=0}^{k−1} A_{i}) ⇒ ((A_{k} ⇒ ∀Q.¬A_{k}) ⊓ (¬A_{k} ⇒ ∀Q.A_{k}))) ,

C′′= ⨅_{k=0}^{n−1} ∀R.∀R^{−} .( ( ⨆_{i=0}^{k−1} ¬A_{i}) ⇒ ((A_{k} ⇒ ∀Q.A_{k}) ⊓ (¬A_{k} ⇒ ∀Q.¬A_{k})))

and C ⇒ D is an abbreviation for ¬C ⊔ D. It is not hard to see that C_{0} is of size O(n^{2}) and that every model of R satisfying C_{0} has a Q-path of length 2^{n}. For n = 3, such a model I is shown below, where x_{0} ∈ (¬A_{2} ⊓ ¬A_{1} ⊓ ¬A_{0})^{I} , x_{1} ∈ (¬A_{2} ⊓ ¬A_{1} ⊓ A_{0})^{I} , x_{2} ∈ (¬A_{2} ⊓ A_{1} ⊓ ¬A_{0})^{I} , …, x_{7} ∈ (A_{2} ⊓ A_{1} ⊓ A_{0})^{I} .

x_{0} y x_{1} x_{2} x_{3} x_{4} x_{5} x_{6} x_{7} R R^{−} Q R^{−} Q R^{−} Q R^{−} Q R^{−} Q R^{−} Q R^{−} Q Q

In other words, the concepts A_{n−1} , …, A_{0} encode the bits of an n-bit binary counter, with A_{0} representing the least significant bit and A_{n−1} the most significant one.

Theorem 3.1. Concept satisfiability w.r.t. ALCIr-RBoxes is ExpTime-hard.

Proof. The proof is by encoding computations of alternating Turing machines with a polynomial tape. Recall [6] that an alternating Turing machine (ATM) is a quadruple of the form M = (Q, Σ, q_{0}, δ), where Q = Q_{∃} ⊎Q_{∀} ⊎{q_{a}}⊎{q_{r}} is a finite set of states containing existential states Q_{∃}, universal states Q_{∀}, an accepting state q_{a} and a rejecting state q_{r}; Σ = {a_{0}, …, a_{n−1} , b} is a tape alphabet with a special symbol b for ‘blank’; q_{0} ∈ Q_{∃} ⊎ Q_{∀} is an initial state; and

δ: (Q ∖ {q_{a}, q_{r}}) × Σ → (Q × Σ × {l, r})^{2}

is a transition function that, for any q ∈ Q∖{q_{a}, q_{r}} and a ∈ Σ, gives two alternative transitions. If δ(q, a) = ((q_{1}, a_{1}, d_{1}), (q_{2}, a_{2}, d_{2})), then we write δ_{i}(q, a) = (q_{i}, a_{i}, d_{i}), for i = 1, 2.

A configuration of an ATM M is a word wqw′, where q ∈ Q and w, w′ ∈ Σ^{∗}; it represents the situation when the tape contains the word ww′, the machine is in state q, with its head scanning the first symbol of w′. The successor configurations of wqw′ are defined in the usual way in terms of the transition function δ (where l and r instruct the head to move one cell to the left or, respectively, to the right). A halting configuration is of the form wqw′ with q ∈ {q_{a}, q_{r}}.

A computation path of M on a word w ∈ Σ^{∗} is a sequence of configurations c_{1}, c_{2}, … such that c_{1} = q_{0}w and, for i ⩾ 1, c_{i+1} is a successor configuration of c_{i}. We assume that there is a polynomial function p such that M uses at most p(m) tape cells on any input of length m and that every computation path of M is of length ⩽ 2^{p(m)} . A halting configuration is accepting if it is of the form wq_{a}w′. For a non-halting configuration c = wqw′, we define (inductively) c to be accepting if either q ∈ Q_{∃} and at least one of the successor configurations of c is accepting, or q ∈ Q_{∀} and both the successor configurations are accepting. Finally, we say that M accepts an input w if the initial configuration q_{0}w is accepting. We use L(M) to denote the language accepted by M, that is, L(M) = {w ∈ Σ^{∗} | M accepts w}. It is well known [6] that the acceptance problem for such ATMs is ExpTime-complete.

Now, given an ATM M and a word w = x_{0} ⋯ x_{n−1} ∈ Σ^{∗}, we construct a concept C_{0} and an RBox R in ALCIr such that w ∈ L(M) iff C_{0} is satisfiable w.r.t. R. To achieve this, we use Example 3.1 to represent successive configurations of M by individuals of models of R satisfying C_{0} and arrange them in a binary tree-like structure with branching factor 2 and depth ⩽ 2^{p(n)} .

Consider the RBox

R = {R ⊑ Q_{1}R, R ⊑ Q_{2}R}.

We use the role name Q_{j}, j = 1, 2, to connect two successive configurations c and c′ such that c′ is obtained from c by means of the jth component of the pair δ(q, a) that is applicable to c. We require the following concept names:

– A to say that a configuration is accepting;

– B_{q}, for q ∈ Q, to say that the current state is q;

– H_{i}, for i ⩽ p(n), to say that the head is currently scanning cell i;

– D_{a}^{i}, for a ∈ Σ and i ⩽ p(n), to say that the current symbol in the ith cell is a;

– A_{i}, for i < p(n), to encode the binary counter;

– E to say that an object is a Q_{1}-successor of its parent;

– F ≡ (A_{p(n)−1} ⊓ ⋯⊓ A_{0}) to say that an object is a leaf. To construct the required binary tree-like structure, we use the following concept C_{T}, where C ⇔ D stands for (C ⇒ D) ⊓ (D ⇒ C):

C_{T} = C^{zero} ⊓ C^{F} ⊓ ∃R.⊤ ⊓ ⨅_{j=1}^{2}(C′_{j} ⊓ C′′_{j}⊓ C′′′_{j}),

where

C^{zero} = ¬A_{p(n)−1} ⊓ ⋯⊓ ¬A_{0},
C^{F} = ∀R.∀R^{−} .(F ⇔ (A_{p(n)−1} ⊓ ⋯⊓ A_{0})),
C′_{j} = ⨅_{k=0}^{p(n)−1} ∀R.∀R^{−} .(F ⊔ C_{k,j}^{invert} ),

C_{k,j}^{invert} = ( ⨅_{i=0}^{k−1} A_{i}) ⇒ ( (A_{k} ⇒ ∀Q_{j} .¬A_{k}) ⊓ (¬A_{k} ⇒ ∀Q_{j} .A_{k})) ,

C′′_{j}= ⨅_{k=0}^{p(n)−1} ∀R.∀R^{−} .(F ⊔ C_{k,j}^{retain} ),

C_{k,j}^{retain} = ( ⨆_{i=0}^{k−1} ¬A_{i}) ⇒ ( (A_{k} ⇒ ∀Q_{j} .A_{k}) ⊓ (¬A_{k} ⇒ ∀Q_{j} .¬A_{k})) ,
C′′′_{1}= ∀R.∀R^{−} .∀Q_{1}.E,  C′′′_{2}= ∀R.∀R^{−} .∀Q_{2}.¬E.

It is not hard to see that there is a model of R satisfying C_{T} that contains the full binary tree of depth 2^{p(n)} − 1 every non-leaf node of which has distinct Q_{1}-and a Q_{2}-successors.

We now construct the concept C_{0} by giving its subconcepts. The concept C^{ini} defines the initial configuration. C_{(q,i,a)}^{l} and C_{(q,i,a)}^{r} describe the movements of the head to the left and right. C_{nh} makes sure that the symbols that are not in the active cell do not change. C_{dfh}, C_{dfq} and C_{dfs} ensure uniqueness of the head position, current state and symbol in the active cell. C_{acc} describes accepting configurations using concepts C_{∀} and C_{∃}. These concepts are defined as follows:

C^{ini} = B_{q_{0}} ⊓ H_{0} ⊓ ( ⨅_{i=0}^{n−1} D_{x_{i}}^{i} ) ⊓ ( ⨅_{i=n}^{p(n)} D_{b}^{i}) ,

C_{(q,i,a)}^{r} = (B_{q} ⊓ H_{i} ⊓ D_{a}^{i}) ⇒ ( ⨅_{t∈{1,2}, δ_{t}(q,a)=(q′,a′,r)} ∀Q_{t}.(B_{q′} ⊓ H_{i+1} ⊓ D_{a′}^{i})) ,

C_{(q,i,a)}^{l} = (B_{q} ⊓ H_{i} ⊓ D_{a}^{i}) ⇒ ( ⨅_{t∈{1,2}, δ_{t}(q,a)=(q′,a′,l)} ∀Q_{t}.(B_{q′} ⊓ H_{i−1} ⊓ D_{a′}^{i})) ,
C_{nh} = ⨅_{a∈Σ, 0⩽i,j⩽p(n), i≠j} ∀R.∀R^{−} .((H_{j} ⊓ D_{a}^{i}) ⇒ (∀Q_{1}.D_{a}^{i} ⊓ ∀Q_{2}.D_{a}^{i})),
C_{dfh} = ⨅_{0⩽j<i⩽p(n)} ∀R.∀R^{−} .(¬H_{j} ⊔ ¬H_{i}),
C_{dfq} = ⨅_{q,q′∈Q, q≠q′} ∀R.∀R^{−} .(¬B_{q} ⊔ ¬B_{q′}),
C_{dfs} = ⨅_{a,b∈Σ, a≠b, 0⩽i⩽p(n)} ∀R.∀R^{−} .(¬D_{a}^{i} ⊔ ¬D_{b}^{i}),
C_{∀} = ⨆_{q∈Q_{∀} , a∈Σ, 0⩽i⩽p(n)} (B_{q} ⊓ H_{i} ⊓ D_{a}^{i} ⊓ ∀Q_{1}.A ⊓ ∀Q_{2}.A),
C_{∃} = ⨆_{q∈Q_{∃} , a∈Σ, 0⩽i⩽p(n)} (B_{q} ⊓ H_{i} ⊓ D_{a}^{i} ⊓ (∀Q_{1}.A ⊔ ∀Q_{2}.A)),
C_{acc} = A ⊓ ∀R.∀R^{−} .((B_{q_{a}} ⊔ C_{∀} ⊔ C_{∃}) ⇔ A).

Finally, we set

C_{0} = C_{T} ⊓ C^{ini} ⊓ C_{acc} ⊓ C_{dfh} ⊓ C_{dfq} ⊓ C_{dfs} ⊓ C_{nh} ⊓

⨅_{q∈Q, a∈Σ, 0⩽i⩽p(n)−1} ∀R.∀R^{−} .C_{(q,i,a)}^{r} ⊓ ⨅_{q∈Q,a∈Σ,1⩽i⩽p(n)} ∀R.∀R^{−} .C_{(q,i,a)}^{l} .

The size of C_{0} is O(p(n)^{2}), and one can check that C_{0} is satisfiable w.r.t. R iff the ATM M accepts input w. □

The precise complexity of concept satisfiability w.r.t. ALCIr RBoxes is still unknown. As shown by Example 3.1 and the proof above, models of R satisfying C_{0} can be of exponential width. The tableau algorithm for SR^{+} OIQ from [13] indicates that, for this more powerful language, we can expect multiple exponential blowups of the depth. However, we hope that this does not happen for ALCIr and conjecture that concept satisfiability w.r.t. ALCIr RBoxes is ExpTime-complete. Some grounds for this conjecture will be given in the next section, where we define a non-trivial fragment of ALCIr for which this problem turns out to be PSpacecomplete.

4. Description Logic ALCIr^{−}

Let R be an ALCIr RBox and C_{0} an ALCIr concept. To simplify presentation, and without loss of generality, we can assume that all RIs are of the form R ⊑ QP. Let R = {r_{i} | i = 1, …, l}, where r_{i} = (R_{i} ⊑ Q_{i}P_{i}), for i = 1, …, l. We denote by ALCIr^{−} the fragment of ALCIr in which RBoxes are such that no role name rn(P_{i}), for i = 1, …, l, occurs on the left-hand side of RIs (that is, rn(P_{i}) ≠ rn(R_{j}) for any i, j ⩽ l). Our aim in this section is to develop a tableau algorithm for this DL that works in the polynomial space. This algorithm can be obtained by properly modifying the tableau algorithm for SR^{+} OIQ given in [13]. So, we begin by reminding the reader of the basic definitions and notation used [13].

4.1. Quasi-Concepts. First we define a set qc(C_{0}, R) the elements of which are called quasi-concepts (for C_{0} w.r.t. R); we need them in labels for tableau nodes. In the definition of qc(C_{0}, R), we require a dependency relation ◁ on R, which is defined by taking r_{i} ◁ r_{j} if rn(R_{i}) = rn(Q_{j}). The following lemma shows that the transitive closure of ◁ is acyclic:

Lemma 4.1. [13] (i) If r_{i} ◁ r_{j}, then r_{j} ◁ r_{i} does not hold.
(ii) If r_{i_{1}} ◁ r_{i_{2}} and r_{i_{2}} ◁ r_{i_{3}} , then r_{i_{3}} ◁ r_{i_{1}} does not hold.

For a set Σ ⊆ con(C_{0}) and a basic role P, we set Σ|_{P}^{∀} = {C | ∀P.C ∈ Σ}. Sometimes it will be convenient to write qc(r_{0}) in place of con(C_{0}) and assume that r_{0} ◁ r_{i}, for 1 ⩽ i ⩽ l. Now, assuming that qc(r_{j}) is defined for every r_{j} ◁ r_{i} with 0 ⩽ i, j ⩽ l, we define qc(r_{i}) to be the set of all ∀R_{i}.∃P_{i}^{−} .(t^{r}, t^{∀}, t^{−} ) such that

t^{r} = Q_{i},  t^{∀} ⊆ ⋃_{r_{j} ◁r_{i}} qc(r_{j})|_{t^{r}}^{∀} ,  t^{−} ⊆ ⋃_{r_{j} ◁r_{i}} qc(r_{j})|_{inv(t^{r} )}^{∀}.

For Σ(r_{i}) ⊆ qc(r_{i}) and a basic role P, let

Σ(r_{i})|_{P}^{∀} = {∃P_{i}^{−} .(t^{r}, t^{∀}, t^{−} ) | ∀R_{i}.∃P_{i}^{−} .(t^{r}, t^{∀}, t^{−} ) ∈ Σ(r_{i}) and P = R_{i}}.

Finally, we set qc(C_{0}, R) = ⋃ _{i=0}^{l} qc(r_{i}), and, for Σ ⊆ qc(C_{0}, R) and a basic role P,

Σ|_{P}^{∀} = ⋃_{j=0}^{l} (Σ ∩ qc(r_{j}))|_{P}^{∀}.

For Σ ⊆ qc(C_{0}, R) and 1 ⩽ i ⩽ l, let Ξ(r_{i}, Σ) = ∃P_{i}^{−} .(t^{r}, t^{∀}, t^{−} ), where t^{r} = Q_{i}, t^{∀} = Σ|_{t^{r}}^{∀} , t^{−} = Σ ∩ qc(C_{0}, R)|_{inv(t^{r} )}^{∀}.

4.2. Tableaux and Concept Tableaux. A tableau for C_{0} w.r.t. R is a structure of the form T = (S, ℓ, E), where S is a nonempty set, ℓ: S → 2^{qc (C_{0} ,R)} and E: role(C_{0}, R) → 2^{S ×S} are such that the following conditions hold:

p1: C_{0} ∈ ℓ(u_{0}), for some u_{0} ∈ S,

p2: if C ∈ ℓ(u), then ¬C ∉ ℓ(u), where C is a concept name,

p3: ⊤ ∈ ℓ(u) and ⊥ ∉ ℓ(u) for any u,

p4: if (C_{1} ⊓ C_{2}) ∈ ℓ(u), then C_{1} ∈ ℓ(u) and C_{2} ∈ ℓ(u), p5: if (C_{1} ⊔ C_{2}) ∈ ℓ(u), then C_{1} ∈ ℓ(u) or C_{2} ∈ ℓ(u), p6: if ∃R.C ∈ ℓ(u), then there is some v ∈ S with (u, v) ∈ E(R) and C ∈ ℓ(v), p7: (u, v) ∈ E(R) iff (v, u) ∈ E(inv(R)), p8: if ∀R.C ∈ ℓ(u) and (u, v) ∈ E(R), then C ∈ ℓ(v), p9: if ∀R.ℭ ∈ ℓ(u) and (u, v) ∈ E(R), then ℭ ∈ ℓ(v), p10: ∀R_{i}.ℭ ∈ ℓ(u), where ℭ = Ξ(r_{i}, ℓ(u)), for all u ∈ S and 1 ⩽ i ⩽ l, p11: if ∃P.(t^{r}, t^{∀}, t^{−} ) ∈ ℓ(u), then there is v with (u, v) ∈ E(P), t^{∀} ⊆ ℓ(v) and

ℓ(v)|_{inv(t^{r} )}^{∀} ⊆ t^{−} .

A concept tableau for C_{0} w.r.t. R is a structure of the form T = (S, 𝔠, E), where S is nonempty set, 𝔠: S → 2^{con (C_{0} )} and E: role(C_{0}, R) → 2^{S ×S} are such that:

a: conditions (p1)–(p8) hold for ℓ replaced by 𝔠; b: if (u, v) ∈ E(R_{i}), then (u, v) ∈ E(Q_{i}) ∘ E(P_{i}).

Theorem 4.1. Suppose C_{0} is an ALCIr concept and R an ALCIr RBox. Then the following conditions are equivalent:

(a) C_{0} is satisfiable w.r.t. R;

(b) there exists a tableau for C_{0} w.r.t. R;

(c) there exists a concept tableau for C_{0} w.r.t. R.

Proof. The equivalence (a) ⇔ (b) follows from [13].

(b) ⇒ (c). Let T = (S, ℓ, E) be a tableau for C_{0} w.r.t. R. Define a concept tableau T′ = (S′, 𝔠, E′) by taking S′ = S, 𝔠(u) = ℓ(u) ∩ con(C_{0}) for all u ∈ S. For a role name R, we define E′(R), by induction on ≺_{R}, as follows:

E′(R)= E(R)

∪ ⋃_{{i|R=Q_{i} }} {(u, v) | ar(R, u, v) & ∃z ((u, z) ∈ E′(R_{i}) ∧ (v, z) ∈ E(P_{i}))}

∪ ⋃_{{i|R=inv(Q_{i} )}}{(u, v) | ar(R, u, v) & ∃z ((v, z) ∈ E′(R_{i}) ∧ (u, z) ∈ E(P_{i}))}.

Here ar(R, u, v) is an abbreviation for ℓ(u)|_{R}^{∀} ⊆ ℓ(v) and ℓ(v)|_{inv(R)}^{∀} ⊆ ℓ(u). We also set E′(inv(R)) = {(u, v) | (v, u) ∈ E′(R)}. It is easy to see that T′ = (S′, 𝔠, E′) is concept tableau for C_{0} w.r.t. R.

(c) ⇒ (b) Let T′ = (S′, 𝔠, E′) be a concept tableau for C_{0} w.r.t. R. Construct a tableau T = (S, ℓ, E) by taking S = S′, E = E′ and defining ℓ as follows. First, we define, by induction on ◁, auxiliary sets ℓ′(u, r), where r is an RI. Recalling that r_{0} ◁ r_{i} for all i, 1 ⩽ i ⩽ l, we set ℓ′(u, r_{0}) = 𝔠(u). Then, assuming that ℓ′(u, r′) is defined for every r′◁ r_{i} , we set

ℓ′(u, r_{i}) = {∀R_{i}.ℭ | ℭ = Ξ(r_{i},_{⋃ r_{′}◁r_{i}} ℓ′(u, r′))}

∪ {ℭ | ∃v ∈ S, (v, u) ∈ E′(R_{i}), ℭ = Ξ(r_{i},_{⋃ r_{′}◁bsr_{i}} ℓ′(v, r′))}.

Finally, we set ℓ(u) = ⋃ _{j=0}^{l} ℓ′(u, r_{j}). One can show now that T is a tableau for C_{0} w.r.t. R. □

4.3. Completion Trees. We are now in a position to define a tableau algorithm for ALCIr. For ALCIr concepts C_{0} and RBoxes R, the algorithm works on completion trees similarly to the algorithms of [2, 13]. To present it, we require some additional notation. For RI r_{i} = (R_{i} ⊑ Q_{i}P_{i}) for 1 ⩽ i ⩽ l, let

qc^{+} (r_{i}) = {∀Q_{i}.ℭ | ∀Q_{i}.ℭ ∈ _{⋃ r_{j} ◁r_{i}} qc(r_{j})},
qc^{−} (r_{i}) = {ℭ | ∀ inv(Q_{i}).ℭ ∈ _{⋃ r_{j} ◁r_{i}} qc(r_{j})},
qc^{∗}(r_{i}) = qc^{+} (r_{i}) ∪ qc^{−} (r_{i}).

The set qc^{∗}(r_{i}) of quasi-concepts is to be guessed by the algorithm. Let \overline{qc}(C_{0}, R) be the minimal set such that:

– qc(C_{0}, R) ⊆ \overline{qc}(C_{0}, R),

– if ∀Q.ℭ ∈ \overline{qc}(C_{0}, R), then ℭ ∈ \overline{qc}(C_{0}, R),
– if ∃P.ℭ ∈ \overline{qc}(C_{0}, R), then ℭ ∈ \overline{qc}(C_{0}, R).

Unlike qc(C_{0}, R), the set \overline{qc}(C_{0}, R) contains sub-quasi-concepts.

Given an ALCIr concept C_{0} and an RBox R, a completion tree for C_{0} and R is a structure of the form T = (V, E, ℓ, 𝔤, 𝔦, 𝔩), where

– (V, E) is a directed tree;

– for each (x, y) ∈ E, we have 𝔩(x, y) ∈ role(C_{0}, R); if 𝔩(x, y) = R, then y is called an R-successor of x; y is called an R-neighbour of x if y is an R-successor of x or x is an inv(R)-successor of y;

– ℓ(x) ⊆ \overline{qc}(C_{0}, R), 𝔤(x) ⊆ ⋃ _{i=1}^{l} qc^{∗}(r_{i}) and 𝔦(x) ⊆ \{1, …, l\}, for x ∈ V. We say that a completion tree T contains a clash if there is x ∈ V such that at least one of the following conditions holds:

– ⊥ ∈ ℓ(x),

– {A, ¬A} ⊆ ℓ(x), for a concept name A,
– i ∈ 𝔦(x) and there exists ℭ ∈ (qc^{∗}(r_{i}) ∩ ℓ(x)) ∖ 𝔤(x),
– ℭ = (t^{r}, t^{∀}, t^{−} ) ∈ ℓ(x) and ℓ(x)|_{inv(t^{r} )}^{∀} ⊈ t^{−} .

A completion tree that does not contain a clash is called clash-free.

To ensure that the tableau algorithm eventually comes to a stop, we use a blocking technique that is similar to the one used in [13]. A node x ∈ V is called blocked if it is either directly or indirectly blocked. A node x ∈ V is directly blocked if none of its (not necessarily immediate) E-ancestors is blocked, and there are nodes x′, y and y′ such that:

– y′ is not a root,

– (x′, x) ∈ E, (y′, y) ∈ E and y is an E-ancestor of x′,

– ℓ(x) = ℓ(y), ℓ(x′) = ℓ(y′) and 𝔩(x′, x) = 𝔩(y′, y). In this case we say that y blocks x. A node y is indirectly blocked if one of its E-ancestors is blocked. (Note that the blocking condition is the same as for SR^{+} OIQ.)

Our tableau algorithm is nondeterministic. It takes an ALCIr concept C_{0} and an RBox R as input and returns ‘yes’ or ‘no’ to indicate whether C_{0} is satisfiable w.r.t. R or not. It starts by constructing the completion tree T = (V, E, ℓ, 𝔤, 𝔦, 𝔩), where V = {x_{0}}, E = ∅, ℓ(x_{0}) = {C_{0}, ⊤}, 𝔤(x_{0}) = ∅, 𝔦(x_{0}) = ∅, 𝔩 = ∅. Then the algorithm non-deterministically applies one of the completion rules given in

Table 1. Completion rules for the ALCIr tableau algorithm.

(⊓)  if C_{1} ⊓ C_{2} ∈ ℓ(x), x is not indirectly blocked and {C_{1}, C_{2}} ⊈ ℓ(x),

then ℓ(x) := ℓ(x) ∪ {C_{1}, C_{2}}

(⊔)  if C_{1} ⊔ C_{2} ∈ ℓ(x), x is not indirectly blocked and

{C_{1}, C_{2}} ∩ ℓ(x) = ∅, then ℓ(x) := ℓ(x) ∪ {D}, for some D ∈ {C_{1}, C_{2}}

(∃_{c})  if ∃S.C ∈ ℓ(x) ∩ con(C_{0}), x is not blocked and

x has no S-neighbour y with C ∈ ℓ(y), then create a new node y ∈ V with 𝔩(x, y) := {S}, ℓ(y) := {C, ⊤}

(∀)  if ∀R.C ∈ ℓ(x), x is not indirectly blocked and

there is an R-neighbour y of x such that C ∉ ℓ(y), then set ℓ(y) := ℓ(y) ∪ {C}

(guess_{r_{i}}) if i ∉ 𝔦(x) and x is not indirectly blocked, then

1) non-deterministic guess k and {ℭ_{1}, …, ℭ_{k}} ⊆ qc^{∗}(r_{i}),

2) set 𝔦(x) := 𝔦(x) ∪ {i}, ℓ(x) := ℓ(x) ∪ {ℭ_{1}, …, ℭ_{k}}, and

3) 𝔤(x) := 𝔤(x) ∪ ℓ(x) ∩ qc^{∗}(r_{i})
(RI_{r_{i}})  if i ∈ 𝔦(x), ∀R_{i}.ℭ ∉ ℓ(x), ℭ = Ξ(r_{i}, ℓ(x)) and

x is not indirectly blocked, then ℓ(x) := ℓ(x) ∪ {∀R_{i}.ℭ}

(∃_{q})  if ∃P.ℭ ∈ ℓ(x), for ℭ = (t^{r}, t^{∀}, t^{−} ), x is not blocked and

x has no P -successor y with ℭ ∈ ℓ(y), then create a new node y ∈ V and set 𝔩(x, y) := {P }, ℓ(y) := {⊤, ℭ}

(qc)  if ℭ ∈ ℓ(x), for ℭ = (t^{r}, t^{∀}, t^{−} ), x is not indirectly blocked

and t^{∀} ⊈ ℓ(x), then set ℓ(x) := ℓ(x) ∪ t^{∀}

Table 1; it keeps doing so till either the current completion graph contains a clash, in which case the answer is ‘no’, or none of the rules is applicable, in which case the algorithm returns ‘yes’.

As a consequence of [13], we obtain:

Lemma 4.2. The tableau algorithm always terminates.

Lemma 4.3. The tableau algorithm returns ‘yes’ iff there is a tableau for C_{0} w.r.t. R.

Remark 4.1. The main difference between the tableau rules in this paper and those in [13] is in the rules (∃_{q}) and (guess_{r_{i}}). The rule (∃_{q}) creates a new node in the case when a certain node has no P -successor, while in [13] a new node was created if there was no P -neighbour. This simplification is possible because ALCIr does not have number restrictions. The analogue of the rule (guess_{r_{i}}) in [13], for every D ∈ qc^{∗}(r_{i}), put either D or ¬D to ℓ(x). Here we only guess a polynomial subset 𝔤(x) of qc^{∗}(r_{i}) and assume that the remaining (possibly exponentially many) quasi-concepts from qc^{∗}(r_{i}) are taken with negations.

In the next two sections, we are going to show that if there is a model of R satisfying C_{0}, then there exists a tableau for C_{0} w.r.t. R of both polynomial width and polynomial depth. These results will be used later to show that to check whether such tableaux exist only the polynomial space is required.

4.4. Polynomial width. Observe first that the set con(C_{0}) we use for labelling the nodes is of size l_{1} = O(|C_{0}|). Note also that the rule ∃_{q} always creates a new node if there is no suitable P -successor, even though a suitable P -predecessor may exist(cf. the tableau rules in [13]). As a results, the completion tree grows in depth rather than in width. More precisely, we have the following:

Lemma 4.4. When applied to C_{0} and R, the tableau algorithm generates at most (l + 1) × l_{1} successors of any node in the completion tree.

Proof. We say that a node x (a node y) in a completion tree is an inv(Q_{j})- implicit neighbour (respectively, a Q_{j} -implicit neighbour) of a node y (respectively,

x) if (i) there is no arc Q_{j} connecting x and y, (ii) there is a predecessor z of y such that x is an inv(R_{j})-neighbour or an inv(R_{j})-implicit neighbour z, and (iii) y has been created by (∃_{q}) applied to z and a quasi-concept ∃ inv(P_{j}).(t^{r}, t^{∀}, t^{−} ), where t^{r} = Q_{j}. (Because of the rule (∃_{q}), in (ii) we do not consider P_{j} -successors of y.)

Successors to a given node can be generated by the rules (∃_{c}) or (∃_{q}). The rule (∃_{c}) generates at most |ℓ(x) ∩ con(C_{0})| < l_{1} successors. On the other hand, a quasi-concept of the form ∃ inv(P_{i}).ℭ can be added to ℓ(x) by the rule (∀) when x has an inv(R_{i})-neighbour. Such a concept can also be added by the rule (qc) if R_{i} = Q_{j}, for some j, and x has an inv(Q_{j})-implicit neighbours or by the rule (guess_{r_{j}} ) if R_{i} = inv(Q_{j}), for some j, and x has an Q_{j} -implicit neighbours. In the latter case (since rn(R_{i}) = rn(Q_{j})), we have r_{i} ◁ r_{j}. Thus, it suffices to compute the number of inv(R_{i})-neighbours (including implicit ones) of a given node. By induction on k, we now prove the following property: if r_{i_{k}} ◁ r_{i_{k−1}} ◁ ⋯◁ r_{i_{1}} is a longest chain of dependent RIs beginning with r_{i_{k}} , then any node in the completion tree can have at most k × l_{1}-many inv(R_{i_{k}} )-neighbours (including implicit ones).

For k = 1, all inv(R_{i_{k}} )-successors are created by the rule (∃_{c}), and so there are at most l_{1}-many inv(R_{i_{k}} )-neighbours. For k > 1, we have at most l_{1}-many inv(R_{i_{k}} )- successors created by the rule (∃_{c}) and at most (k − 1) × l_{1}-many implicit inv(R_{i_{k}} )- neighbours, where rn(Q_{i_{k−1}} ) = rn(R_{i_{k}} ). In total, we have at most k × l_{1}-many inv(R_{i_{k}} )-neighbours. Namely, a node x can have implicit inv(Q_{i_{k−1}} )-neighbours or Q_{i_{k−1}} -neighbours if it has a P_{i_{k−1}} -predecessor y with inv(R_{i_{k−1}} )-neighbours. By IH, the node y can have at most (k − 1) × l_{1}-many inv(R_{i_{k−1}} )-neighbours, and so x can have at most (k − 1) × l_{1} implicit inv(R_{i_{k}} )-neighbours.

Since k ⩽ l, we conclude that the rule (∃_{q}) can create at most l × l_{1} successors of a given node. These neighbours are not affected by the addition of new quasiconcepts of the form ∃ inv(P_{i}).ℭ because P_{i} ≠ R_{j}. Thus, any node can have at most (l + 1) × l_{1} successors. □

4.5. Polynomial depth. Now we prove that if C_{0} is satisfiable w.r.t. R, then it has a finite tableau of both polynomial width and polynomial depth. We do that in three steps.

First, by Lemma 4.4, there is a completion tree whose branching factor is at most (l + 1) × l_{1}. Using this tree, we can construct in the same way as in [13] a possibly infinite tableau T = (S, ℓ, E), which is a tree with branching factor ⩽ (l + 1) × l_{1}. Then, by Theorem 4.1, we can add some edges to T and construct a concept tableau T′ = (S′, 𝔠, E′), where E′ = E_{1} ∪ E_{2}, E_{1} = E and E_{2} = E′∖ E. As the basis of the concept tableau is a tree, we call T′ a quasi-tree concept tableau (QTCT, for short) and write T′ = (S′, 𝔠, E_{1}, E_{2}) instead of T′ = (S′, 𝔠, E′).

Second, we use the QTCT T′ to construct a QTCT \overline{T} of polynomial ‘depth’. We describe this step in more detail. Suppose u_{0} is a root of T′ = (S′, 𝔠, E_{1}, E_{2}). We then say that u_{0} is of depth 0 in T′. Now, a node u ≠ u_{0} is of depth k in T′ if there is a neighbour v of u of depth k − 1 and there is no neighbour of u of depth < k − 1.

For a concept C in NNF, we define its quantifier depth d(C) by taking

d(⊥) = d(⊤) = d(A) = d(¬A) = 0, for A ∈ N_{C};
d(C_{1} ⊓ C_{2}) = d(C_{1} ⊔ C_{2}) = max{d(C_{1}), d(C_{2})};
d(∃R.C) = d(∀R.C) = d(C) + 1.

A set P is called good w.r.t. T′ if either P = {(C_{0}, u_{0})} or P = P′∪ {(C, u)} where P′ is good w.r.t. T′, C ∈ 𝔠(u) and one of the following conditions holds:

– there is a concept C′ of the form C_{1} ⊓ C_{2} or C_{1} ⊔ C_{2}, where C ∈ {C_{1}, C_{2}}, such that (C′, u) ∈ P′

– there exist an inv(R)-neighbour v of u and a concept C′ of the form ∃R.C

or ∀R.C such that (C′, v) ∈ P′.

In either case, we say that the concept C was added to P because of C′. Clearly, if both P and P′ are good w.r.t. T′, then P ∪ P′ is also good w.r.t. T′.

Suppose P is good w.r.t. T′ and u ∈ S. Set d(u, P) = max{d(C) | (C, u) ∈ P} if there is a concept C such that (C, u) ∈ P; otherwise set d(u, P) = 0.

Lemma 4.5. If P = P′ ∪ {(C, u)} is good w.r.t. T′ and C was added to P because of C′, then d(C′) ⩾ d(C).

Proof. If C′ ∈ 𝔠(u) is of the form C_{1} ⊓ C_{2} or C_{1} ⊔ C_{2}, where C ∈ {C_{1}, C_{2}}, then d(C′) = max{d(C_{1}), d(C_{2})} ⩾ d(C).

If C′ ∈ 𝔠(v) has the form ∀R.C or ∃R.C, where v is an inv(R)-neighbour of u, then d(C′) = d(C) + 1 > d(C). □

Lemma 4.6. Suppose P is good w.r.t. T′and u is of depth k in T′. If k ⩽ d(C_{0}), then d(u, P) ⩽ d(C_{0}) − k.

Proof. The proof proceeds by induction on |P|. If P = {(C_{0}, u_{0})}, then the claim holds since, for u ≠ u_{0}, we have d(u, P) = 0 and d(u_{0}, P) = d(C_{0}). Let P = P′∪ {(C, v)}. By IH, d(u, P′) ⩽ d(C_{0}) − k. If v ≠ u, then d(u, P) = d(u, P′) and again the claim holds. If u = v and d(v, P) = d(v, P′), then the claim is obvious.

If u = v and d(v, P) = d(C) > d(v, P′), then C has been added to P because of a concept C′ ∈ 𝔠(u′) of the form ∀R.C or ∃R.C, where u′ is an inv(R)-neighbour of v. We have d(C′) = d(C)+1 > d(C) and u′is of depth k′in T′with k−1 ⩽ k′ ⩽ k+1. So d(u, P) = d(C) = d(C′) − 1 ⩽ d(u′, P′) − 1 ⩽ d(C_{0}) − k′− 1 ⩽ d(C_{0}) − k. □

Corollary 4.1. Suppose P is good w.r.t. T′.

(a) If a node u is of depth k = d(C_{0}) in T′, then d(u, P) = 0.

(b) If u is of depth k > d(C_{0}) in T′, then there is no concept C with (C, u) ∈ P.

Let \overline{P} be a maximal set that is good w.r.t. T′, that is,

\overline{P} = ⋃_{P is good w.r.t. T′} P.

Using the QTCT T′ = (S′, 𝔠, E_{1}, E_{2}) and \overline{P}, we construct \overline{T} = (\overline{S}, \overline{𝔠}, \overline{E_{1}}, \overline{E_{2}}) as follows. Let S_{0} = \{u ∈ S′ | there is a concept C such that (C, u) ∈ \overline{P}\} and \overline{S} be a minimal set such that

– S_{0} ⊆ \overline{S} ⊆ S′,

– if (u, v) ∈ \overline{E}(R_{i}), then (u, v) ∈ \overline{E}(Q_{i}) ∘ \overline{E}(P_{i}),

where, for any role R ∈ role(C_{0}, R) and i = 1, 2, we set \overline{E_{i}}(R) = E_{i}(R) ∩ (\overline{S} × \overline{S}) and \overline{E}(R) = \overline{E_{1}}(R)∪\overline{E_{2}}(R). Finally, we set \overline{𝔠}(u) = \{C | (C, u) ∈ \overline{P}\}∪\{⊤\} for u ∈ \overline{S}.

Theorem 4.2. The structure \overline{T} = (\overline{S}, \overline{𝔠}, \overline{E_{1}}, \overline{E_{2}}) is a QTCT with the following properties:

– Any u ∈ \overline{S} is of depth ⩽ d(C_{0}) + l in \overline{T}.

– Any path from the root node u_{0} to a node u (without repetitions) that uses only \overline{E_{1}}-arcs is of the length ⩽ (d(C_{0}) + l) × (l + 1).

– Any node u ∈ \overline{S} has at most (l + 1) × l_{1}-many \overline{E_{1}}-successors.

Proof. First, we prove that \overline{T} is a concept tableau.

p1: C_{0} ∈ \overline{𝔠}(u_{0}) since (C_{0}, u_{0}) ∈ \overline{P}; p2: holds because \overline{𝔠}(u) ⊆ 𝔠(u); p3: ⊤ ∈ \overline{𝔠}(u) by the definition of \overline{𝔠}(u), and ⊥ ∉ \overline{𝔠}(u) because \overline{𝔠}(u) ⊆ 𝔠(u); p4: if (C_{1} ⊓ C_{2}) ∈ \overline{𝔠}(u) ⊆ 𝔠(u), then (C_{1} ⊓ C_{2}, u) ∈ \overline{P}, C_{1} ∈ 𝔠(u) and C_{2} ∈ 𝔠(u), so \overline{P}∪\{(C_{i}, u)\} is good w.r.t. T′ for i = 1, 2 i.e., (C_{1}, u), (C_{2}, u) ∈ \overline{P}; therefore, C_{1} ∈ \overline{𝔠}(u) and C_{2} ∈ \overline{𝔠}(u);

p5: is similar to (p4);

p6: if ∃R.C ∈ \overline{𝔠}(u) ⊆ 𝔠(u), then (∃R.C, u) ∈ \overline{P} and there is some v ∈ S with (u, v) ∈ E(R) and C ∈ 𝔠(v), so \overline{P} ∪ \{(C, v)\} is good w.r.t. T′, i.e., (C, v) ∈ \overline{P}; therefore, v ∈ \overline{S}, C ∈ \overline{𝔠}(v) and (u, v) ∈ \overline{E}(R);

p7: if (u, v) ∈ \overline{E}(R), then (u, v) ∈ E(R) and u, v ∈ \overline{S}; so (v, u) ∈ E(inv(R))

and (v, u) ∈ \overline{E}(inv(R)); p8: is similar to (p6); b: if (u, v) ∈ \overline{E}(R_{i}), then (u, v) ∈ \overline{E}(Q_{i}) ∘ \overline{E}(P_{i}) by the definition of \overline{S} and

\overline{E}(R).

If u ∈ S_{0}, then, by Lemma 4.6, u is of depth ⩽ d(C_{0}) in \overline{T}. Consider two nodes u, v ∈ \overline{S} whose depth is ⩽ k in \overline{T}. If (u, v) ∈ \overline{E}(R_{i}), then (u, v) ∈ \overline{E}(Q_{i})∘\overline{E}(P_{i}), and so there is z ∈ \overline{S} such that (u, z) ∈ \overline{E}(Q_{i}). Clearly, the depth of z in \overline{T} is ⩽ (k + 1). The arc (u, z) ∈ \overline{E}′(Q_{i}) can require a new node, but only if rn(Q_{i}) = rn(R_{j}). But then we have r_{j} ◁ r_{i}. This means that we can repeat the same procedure at most l times, and so the depth of the new nodes we consider is ⩽ (k + l). Therefore, the depth of u ∈ \overline{S} in \overline{T} is ⩽ d(C_{0}) + l.

Now, consider nodes u, v ∈ \overline{S} whose depth in \overline{T} is k and k + 1, respectively. A path from u to v that uses only \overline{E_{1}}-arcs is of length ⩽ (l+1). Therefore, a path from the root u_{0} to any node u that uses only \overline{E_{1}}-arcs is of the length ⩽ (d(C_{0})+l)×(l+1).

The property that all nodes u ∈ \overline{S} have at most (l+1)×l_{1} \overline{E_{1}}-successors follows from the fact that this property holds for QTCT T′. □

Finally, starting from QTCT \overline{T}, we construct the required tableau by adding appropriate quasi-concepts as described in the proof of the Theorem 4.1. If we omit the arcs from the tableau that belong to \overline{E_{2}}, then we obtain a tree-shaped tableau \overline{T}′. The depth of the tree is bounded by (d(C_{0}) + l) × (l + 1) and the branching factor is bounded by (l + 1) × l_{1}.

By the proof of Lemma 4.4, we conclude that ℓ(x) contains at most l×l_{1} quasiconcepts of the form ∃P.ℭ and there are l quasi-concepts of the form ∀R_{i}.ℭ, that is, there are at most l × (l_{1} + 1) quasi-concepts in ℓ(x). On the other hand, there are at most l_{1} concepts in ℓ(x). Therefore, |ℓ(x)| ⩽ l_{1} + l × (l_{1} + 1).

4.6. PSpace-completeness. PSpace-hardness of concept satisfiability w.r.t. RBoxes in ALCIr^{−} follows from the fact that concept satisfiability in ALC is PSpace-complete. To prove a matching upper bound, we give a nondeterministic algorithm that only requires the polynomial space. The algorithm proceeds in 8 steps:

1. Create a node u_{0}, set u := u_{0} and guess a set ℓ(u_{0}). If C_{0} ∈ ℓ(u_{0}), then go to step 2; otherwise return ‘no’.

2. If the conditions (p2), (p3), (p4), (p5) and (p10) hold for ℓ(u), then go to step 3; otherwise return ‘no’.

3. Set 𝔪(u) := {∃R.C | ∃R.C ∈ ℓ(u)} ∪ {∃P.ℭ | ∃P.ℭ ∈ ℓ(u)}. Guess a non-negative integer k(u) (the number of successors) and go to step 4.

4. If k(u) > 0, then go to step 5; otherwise go to step 6.

5. Create a new node v; set k(u) := k(u)−1. Guess ℓ(v) and R ∈ role(C_{0}, R). Set E(R) := E(R)∪{(u, v)} and E(inv(R)) := E(inv(R))∪{(v, u)}. For all ∃R.C ∈ 𝔪(u), if C ∈ ℓ(v) (i.e., (p6) holds), then 𝔪(u) := 𝔪(u) ∖ {∃R.C}. For all ∃R.(t^{r}, t^{∀}, t^{−} ) ∈ 𝔪(u), if t^{∀} ⊆ ℓ(v) (that is, (p11) holds), then 𝔪(u) := 𝔪(u) ∖ {∃R.(t^{r}, t^{∀}, t^{−} )}. If (p8) and (p9) hold for u and v, set u := v and go to step 2; otherwise return ‘no’.

6. If 𝔪(u) = ∅ go to step 7; otherwise return ‘no’.

7. If u = u_{0} (i.e., u is the root), then return ‘yes’; otherwise go to step 8.

8. If v is a parent of u with (u, v) ∈ E(R), then set E(R) := E(R) ∖ {(u, v)} and E(inv(R)) := E(inv(R)) ∖ {(v, u)}, and set u := v. Go to step 4.

Clearly, the algorithm needs only polynomially space. As NPSpace=PSpace [15], we obtain the following theorem.

Theorem 4.3. Concept satisfiability w.r.t. RBoxes in ALCIr^{−} is PSpacecomplete.

References

1. F. Baader, Restricted role-value-maps in a description logic with existential restrictions and terminological cycles, in: D. Calvanese, G. De Giacomo, E. Franconi (Eds.), Proc. 2003 Internat. Workshop on Description Logics (DL2003).

2. F. Baader, D. Calvanese, D. McGuinness, D. Nardi, P. F. Patel-Schneider, The Description Logic Handbook: Theory, Implementation and Applications, 2nd ed., Cambridge Univ. Press, 2007.

3. C. Bock, X. Zha, H. Suh, J. Lee, Ontological product modeling for collaborative design, Advanced Engineering Informatics 24 (2010), 510–524.

4. R. J. Brachman, J. G. Schmolze, An overview of the KL-ONE knowledge representation system, Cognitive Science 9(2) (1985) 171–216.

5. B. Cuenca Grau, I. Horrocks, B. Motik, B. Parsia, P. Patel-Schneider, U. Sattler, OWL 2: The next step for OWL, J. Web Semantics 6(4) (2008), 309–322.

6. A. K. Chandra, D. C. Kozen, and L. J. Stockmeyer, Alternation, J. ACM 28(1) (1981), 114– 133.

7. S. Demri, The complexity of regularity in grammar logics and related modal logics, J. Log. Comput. 11(6) (2001), 933–960.

8. I. Horrocks, O. Kutz, U. Sattler, The irresistible SRIQ , in: B. Cuenca Grau, I. Horrocks, B. Parsia, P. Patel-Schneider (Eds.), Proc. OWLED*05 Workshop on OWL, Experiences and Directions,

9. , The even more irresistible SROIQ , in: P. Doherty, J. Mylopoulos, C. Welty (eds.), Principles of Knowledge Representation and Reasoning: Proc. Tenth Internat. Conf. (KR-06), 57–67,

10. I. Horrocks, U. Sattler, Decidability of SHIQ with complex role inclusion axioms Artif. Intell. 160(1-2) (2004), 79–104.

11. Y. Kazakov, An extension of complex role inclusion axioms in the description logic SROIQ . in: J. Giesl, R. Hähnle (Eds.), Automated Reasoning, 5th Internat. Joint Conf., IJCAR 2010, Lect. Notes Comput. Sci., Springer-Verlag, 2010, 472–486,.

12. N. Krdžavac, C. Bock, Reasoning in manufacturing part-part examples with OWL2, U.S. National Institute of Standards and Technology, Gaithersburg, U.S.A, 2008.

13. M. Mosurović, N. Krdžavac, H. Graves, M. Zakharyaschev, A Decidable Extension of SROIQ with Complex Role Chains and Unions, J. Artif. Intell. Res. (JAIR) 47 (2013), 809–851.

14. A. Rector, Analysis of propagation along transitive roles: formalisation of the GALEN experience with medical ontologies, in: I. Horrocks, S. Tessaris (Eds.), Proc 2002 International Workshop on Description Logics (DL2002).

15. W. J. Savitch, Relationships between nondeterministic and deterministic tape complexities, J. Comp. System Sci. 4 (1970), 177–192.

16. M. Schmidt-Schauß, Subsumption in KL-ONE is undecidable, in: H. J. Levesque (Ed.), Proc. First Internat. Conf. on Principles of Knowledge Representation and Reasoning, M. Kaufmann, 1989, 421–431.

Faculty of Mathematics and Natural Science (Received 29 09 2013) University of Montenegro Podgorica, Montenegro

 milenko@ac.me

Department of Computer Science and Information Systems Birkbeck, University of London, U.K.

 michael@dcs.bbk.ac.uk