We show that the description logic SOQ with number restrictions on transitive roles is decidable by a terminating tableau calculus. The language decided by the calculus includes the universal role, which allows us to internalize TBox axioms. Termination of the system is achieved through pattern-based blocking.
Efficient tableau algorithms are available for a wide range of description logics,
including logics that contain both transitive roles and functional or number
restrictions, like SIN [
We consider the logic SOQ with number restrictions on transitive roles, and
call it SOQ+. As indicated by its name, SOQ+ extends the basic description
logic ALC [
For termination, our calculus employs pattern-based blocking. Pattern-based
blocking is introduced in [
Following [
We employ three kinds of variables: Nominals x, y, z of type I (we assume there are infinitely many nominals), propositional variables p, q of type IB, and role variables r of type IIB. Since the language in question contains no role expressions other than role variables, we call role variables roles for short. We use the logical constants ⊥, ⊤ : B, ¬ : BB, ∨, ∧, →: BBB, =. : IIB, ∃, ∀ : (IB)B. Terms are defined as usual. We write st for applications, λx.s for abstractions, and s1s2s3 for (s1s2)s3. We also use infix notation, e.g., s ∧ t for (∧)st.
Terms of type B are called formulas. We employ some common notational . . conventions: ∃x.s for ∃(λx.s), ∀x.s for ∀(λx.s), and x6=y for ¬(x=y).
Let us write ∃X.s for ∃x1 . . . xn.s if |X | = n and X = {x1, . . . , xn}. Also, given a set X of nominals, we use the following abbreviation: We use the following constants, which we call modal operators.
DX :=
^ x6=. y x,y∈X x6=y ¬˙p = λx.¬px p ∧˙ q = λx. px ∧ qx p ∨˙ q = λx. px ∨ qx hrinp = λx.∃Y. DY ∧ (Vy∈Y rxy ∧ py) [r]np = λx.∀Y. (Vy∈Y rxy) ∧ DY → Wy∈Y py Enp = λx.∃Y. DY ∧ Vy∈Y py Anp = λx.∀Y. DY → Wy∈Y py
.
x˙ = λy.x=y
T r = ∀xyz.rxy ∧ ryz → rxz
¬˙ : (IB)IB
∧˙ : (IB)(IB)IB
∨˙ : (IB)(IB)IB
h in : (IIB)(IB)IB
[ ]n : (IIB)(IB)IB
En : (IB)IB
An : (IB)IB
˙ : IIB
T : (IIB)B
where |Y | = n + 1 in all equations
To the right of each constant is an equation defining its semantics. Formulas of
the form [r]ntx are called box formulas or boxes, and formulas hrintx are called
diamond formulas or diamonds. The semantics of boxes and diamonds is defined
following [
We assume the application of modal operators to have a higher precedence than regular functional application. So, for instance, we write ¬˙hri2y˙ ∨˙ p x for ((¬˙ (hri2(y˙))) ∨˙ p)x.
A modal interpretation M is an interpretation of simple type theory that interprets B as the set {0, 1}, ⊥ as 0 (i.e., false), ⊤ as 1 (i.e., true), maps I . to a non-empty set, gives the logical constants ¬, ∧, ∨, →, ∃, ∀, = their usual meaning, and satisfies the equations defining the modal operators ¬˙, ∧˙, ∨˙, h in, [ ]n, E, A, ˙ and T . If Mt = 1, we say that M satisfies t. A formula is called satisfiable if it has a satisfying modal interpretation. 3
For the sake of simplicity, we will define our tableau calculus T on negation normal modal expressions, i.e., terms of the form:
t ::= p | ¬˙p | x˙ | ¬˙x˙ | t ∧˙ t | t ∨˙ t | hrint | [r]nt | Ent | Ant A branch Γ is a finite set of formulas s of the form . .
s ::= tx | rxy | T r | x=y | x6=y | ⊥ | α:[r]ntx where t is a negation normal modal expression. The new form α:[r]ntx serves algorithmic purposes. The label α of such label introductions is taken from a countably infinite set of labels. Formulas of the form rxy are called edges. We use the formula ⊥ to explicitly mark unsatisfiable branches. We call a branch Γ closed if ⊥ ∈ Γ . Otherwise, Γ is called open. An interpretation M satisfies a branch Γ if M satisfies all proper formulas on Γ , i.e., all formulas except for label introductions. The branch consisting of the initial formulas to be tested for satisfiability is called the initial branch. Initial branches must contain no edges or label introductions. This restriction is inessential for the expressiveness of the language since label introductions are semantically irrelevant, and edges rxy can equivalently be expressed as hri0y˙x.
Let Γ be a branch. With ∼Γ we denote the least equivalence relation ∼ on . nominals such that x ∼ y for every equation x=y ∈ Γ . We define the equational closure Γ˜ of a branch Γ as Γ˜ := Γ ∪ {tx | ∃x′ : x′ ∼Γ x ∧ tx′ ∈ Γ }
∪ {rxy | ∃x′, y′ : x′ ∼Γ x ∧ y′ ∼Γ y ∧ rx′y′ ∈ Γ } 4
The proof of model existence for our calculus T proceeds in three stages. Applied to a satisfiable initial branch, the rules of T (defined in Sect. 5) construct a quasievident branch (defined in Sect. 6). We show that every quasi-evident branch can be extended to a pre-evident branch, which, in turn, can be extended to an evident branch. For evident branches, we show model existence.
We write DΓ X as an abbreviation for ∀x, y ∈ X : x 6= y ⇒ x6=. y ∈ Γ . A branch Γ is called evident if it satisfies all of the following evidence conditions: (t1 ∧˙ t2)x ∈ Γ ⇒ t1x ∈ Γ˜ ∧ t2x ∈ Γ˜ (t1 ∨˙ t2)x ∈ Γ ⇒ t1x ∈ Γ˜ ∨ t2x ∈ Γ˜ hrintx ∈ Γ ⇒ ∃Y : |Y | = n + 1 ∧ DΓ Y ∧ {rxy, ty | y ∈ Y } ⊆ Γ˜ [r]ntx ∈ Γ ⇒ |{y | rxy ∈ Γ˜, ty ∈/ Γ˜}/∼Γ | ≤ n Entx ∈ Γ ⇒ ∃Y : |Y | = n + 1 ∧ DΓ Y ∧ {ty | y ∈ Y } ⊆ Γ˜ Antx ∈ Γ ⇒ |{y | ty ∈/ Γ˜}/∼Γ | ≤ n
x˙ y ∈ Γ ⇒ x ∼Γ y ¬˙x˙ y ∈ Γ ⇒ x 6∼Γ y
. x=y ∈ Γ ⇒ x ∼Γ y
. x6=y ∈ Γ ⇒ x 6∼Γ y ¬px ∈ Γ ⇒ px ∈/ Γ˜
T r ∈ Γ ⇒ ∀x, y, z : rxy ∈ Γ˜ ∧ ryz ∈ Γ˜ ⇒ rxz ∈ Γ˜ A formula s is called evident on Γ if Γ satisfies the right-hand side of the evidence condition corresponding to s. For instance, (t1 ∧˙ t2)x is evident on Γ if and only if {t1x, t2x} ⊆ Γ˜.
Theorem 4.1 (Model Existence). Evident branches are satisfiable.
Proof. Omitted for space reasons. Proceeds similarly to the argument in [
To simplify the treatment of transitivity, we introduce the notion of preevidence. We define the relation ⊲rΓ as the least relation such that: rxy ∈ Γ˜ ⇒ x ⊲rΓ y x ⊲rΓ y ∧ y ⊲rΓ z ∧ T r ∈ Γ ⇒ x ⊲rΓ z We write x DrΓ y iff x ∼Γ y or x ⊲rΓ y.
The pre-evidence conditions are obtained from the evidence conditions by omitting the condition for transitivity assertions and replacing the condition for boxes as follows:
[r]ntx ∈ Γ ⇒ |{y | x ⊲rΓ y, ty ∈/ Γ˜}/∼Γ | ≤ n Pre-evidence of individual formulas is defined analogously to the corresponding evidence condition. Note that for all formulas but boxes and transitivity assertions, the notions of evidence and pre-evidence coincide.
We now show that every pre-evident branch can be extended to an evident branch. Let the evidence closure Γˆ of a branch Γ be defined as Γ ∪{rxy | x ⊲rΓ y}. Proposition 4.1. rxy ∈ Γˆ ⇐⇒ rxy ∈ Γˆ˜ ⇐⇒ x ⊲rΓ y Theorem 4.2 (Evidence Completion). Γ pre-evident =⇒ Γˆ evident Proof. Omitted for space reasons. Uses Proposition 4.1. ⊓⊔
The tableau rules of our calculus T are defined in Fig. 1. In the rules, we write ∃x ∈ X : Γ (x) for Γ (x1) | . . . | Γ (xn), where X = {x1, . . . , xn} and Γ (x) is a set of formulas parametrized by x. In case X = ∅, the notation translates to ⊥. Dually, we write ∀x ∈ X : Γ (x) for Γ (x1), . . . , Γ (xn) (X = {x1, . . . , xn}).
Given a term t, we write N t for the set of nominals that occur in t. The notation is extended to sets of terms in the natural way: N Γ := S{N t | t ∈ Γ }.
The side condition of R♦ uses the notion of quasi-evidence, which we will introduce in Sect. 6. For now, assume the rule is formulated with the restriction “hrintx not evident on Γ ”.
Given a branch Γ , we define x:Γ α :⇔ ∃y, t : α:ty ∈ Γ ∧ y ⊲rΓ x. A box formula tx is subsumed on Γ if there is a nominal y and a label α such that y DrΓ x and α:ty ∈ Γ . The rule RT is constrained to be applicable only to boxes that are not subsumed on Γ . This ensures, in particular, that RT is applied at most once to each individual box formula on the branch.
A branch Γ is called a proper extension of a branch Δ if Γ ⊇ Δ and Γ˜ ) Δ˜. Note that if Γ is a proper extension of Δ, then in particular it holds Γ ) Δ. We implicitly restrict the applicability of the tableau rules such that a rule R is only applicable to a formula s ∈ Γ if all of the alternative branches Δ1, . . . , Δn resulting from this application are proper extensions of Γ .
Proposition 5.1 (Soundness). Let Δ1, . . . , Δn be the branches obtained from a branch Γ by a rule of T . Then Γ is satisfiable if and only if there is some i ∈ {1, . . . , n} such that Δi is satisfiable. 6
The restrictions on the applicability of the tableau rules given by the pre-evidence conditions are not sufficient for termination. To obtain a terminating calculus, we restrain the rule R♦ by weakening the notion of pre-evidence for diamond formulas. The weaker notion, called quasi-evidence, is then used in the side condition of R♦ in place of pre-evidence. Quasi-evidence must be weak enough to guarantee termination but strong enough to preserve completeness.
The edge graph of a branch Γ is a labelled graph with the nodes N Γ and edges {(x, y) | ∃r : rxy ∈ Γ }, where a node x is labelled with all expressions t such that tx ∈ Γ , and an edge (x, y) is labelled with all roles r such that rxy ∈ Γ . A branch can always be represented graphically through its edge graph.
In [
(s ∧˙ t)x R∧˙ sx, tx
(s ∨˙ t)x
R∨˙ sx | tx hrintx R♦ ∀y, z ∈ Y, y 6= z : y6 =.z, rxy, ty
R [r]ntx
. ∃y, z ∈ Y, y 6= z : y=z | ∃y ∈ Y : ty
RT
T r, rxy α:[r]ntx
Entx ∀y, z ∈ Y, y 6= z : y6 =.z, ty RE RA RN
Y fresh, |Y | = n + 1, hrintx not quasi-evident on Γ
Y ⊆ {y | x ⊲rΓ y}, |Y | = |Y /∼Γ | = n + 1 α fresh, [r]ntx ∈ Γ˜, [r]ntx not subsumed on Γ
Y fresh, |Y | = n + 1, Entx not evident on Γ
Y ⊆ N Γ, |Y | = |Y /∼Γ | = n + 1
.
R6 =⊥. x6=y x ∼Γ y ⊥ Antx
. ∃y, z ∈ Y, y 6= z : y=z | ∃y ∈ Y : ty x˙ y . x=y
¬˙ x˙ y RN¯ x6=y .
R¬⊥˙ ¬˙ px px ∈ Γ˜ ⊥ Γ is the branch to which a rule is applied. “α fresh” stands for ∄t, x : α:tx ∈ Γ “Y fresh” stands for Y ∩ N Γ = ∅. Then all r-diamonds and r-boxes sx ∈ Γ˜ can be made evident by extending Γ with {rxz | ryz ∈ Γ˜}. As an example, consider the edge graph in Fig. 2(a). There, the formula hri0px can be made evident by adding the edge rxz (represented by the dashed arrow) to the branch. In the presence of transitivity, extending a branch Γ by an edge rxz may destroy the evidence of r-boxes tu such that u ⊲rΓ x (Fig. 2(b)). Note, however, that adding an edge rxz cannot destroy the evidence of a box tu such that u ⊲rΓ x if we already have u ⊲rΓ z (Fig. 2(c)).
To deal with non-local constraints introduced by number restrictions on
transitive roles, we refine the notion of a pattern and the quasi-evidence conditions
from [
Given a role r, an r-pattern is a set consisting of modal expressions of the form μt, where μ ∈ {hrin, [r]n | n ∈ IN}, and labels α, such that, for some n, t, x: α:[r]ntx ∈ Γ . We write PΓr x for the largest r-pattern P such that P ⊆ {μt | μtx ∈ Γ˜}∪{α | x:Γ α}. We call PΓr x the r-pattern of x on Γ . An r-pattern P is expanded on Γ if there are nominals x, y such that rxy ∈ Γ˜ and P ⊆ PΓr x. In this case, we say that the nominal x expands P on Γ .
A diamond hrinsx ∈ Γ is quasi-evident on Γ if it is either evident on Γ or x has no r-successor on Γ and PΓr x is expanded on Γ . The rule R♦ can only be applied to diamonds that are not quasi-evident. Note that whenever hrinsx ∈ Γ is quasi-evident but not evident (on Γ ), there is a nominal y that expands PΓr x.
The quasi-evidence conditions are obtained from the pre-evidence conditions by replacing the condition for diamond formulas and adding a condition for transitivity assertions and label introductions as follows: hrintx ∈ Γ ⇒ hrintx is quasi-evident on Γ
T r ∈ Γ ⇒ ∀n, t, x : [r]ntx ∈ Γ˜ ⇒ ∃z, α : z DrΓ x ∧ α:[r]ntz ∈ Γ α:tx ∈ Γ ⇒ tx ∈ Γ ∧ ∀y : x ⊲rΓ y ⇔ y:Γ α Lemma 6.1. Let Γ be a branch. Let {[r]ntx, [r]nty} ⊆ Γ˜ such that T r ∈ Γ and x DrΓ y. Then: [r]ntx is pre-evident on Γ =⇒ [r]nty is pre-evident on Γ Lemma 6.2. Let Γ be a quasi-evident branch. Let hrinsx ∈ Γ be not evident on Γ , y be a nominal that expands PΓr x on Γ , and Δ := Γ ∪ {rxz | ryz ∈ Γ˜}. Then: 1. ∀z : rxz ∈ Δ˜ ⇐⇒ ryz ∈ Γ˜ and x ⊲rΔ z ⇐⇒ y ⊲rΓ z, 2. ∀m, t : hrimt ∈ PΓr x =⇒ hrimtx is evident on Δ, 3. hrinsx is evident on Δ, 4. ∀r′, m, t, z : hr′imtz is evident on Γ =⇒ hr′imtz is evident on Δ, 5. Δ is quasi-evident.
Proof. Omitted for space reasons. Uses Lemma 6.1. ⊓⊔ For an illustration of Lemma 6.2, let the edge graph in Fig. 2(a) (without the dashed arrow) represent Γ . Then hri0px is quasi-evident but not evident on Γ , and y expands PΓr x. The graph with the dashed arrow added corresponds to the branch Δ in the lemma. The five claims for Γ and Δ are easy to verify. Theorem 6.1 (Pre-evidence Completion). For every quasi-evident branch Γ there is a pre-evident branch Δ such that Γ ⊆ Δ.
Proof. Analogous to the corresponding proof in [
A branch is called maximal if it cannot be extended by any tableau rule. Lemma 6.3. Let Γ be a branch that is obtained from an initial branch. Then Γ satisfies the quasi-evidence condition for label introductions.
Proof. Let Γ0 → . . . → Γn be a derivation such that Γ0 is an initial branch and Γn = Γ . The claim is shown by induction on n. ⊓⊔ Theorem 6.2 (Quasi-evidence). Every open and maximal branch obtained in T from an initial branch is quasi-evident.
Proof. Let Γ be an open and maximal branch obtained from an initial branch. We show that every s ∈ Γ that is not of the form px or rxy is either preevident or quasi-evident on Γ by induction on the size of s. The quasi-evidence of formulas α:tx follows by Lemma 6.3. ⊓⊔ 7
We will now show that every tableau derivation is finite. Since the tableau rules are all finitely branching, by K¨onig’s lemma it suffices to show that the construction of every individual branch terminates. Since rule application always produces proper extensions of branches, it then suffices to show that the size (i.e., cardinality) of an individual branch is bounded. First, we show that the size of a branch Γ is bounded by a function in the number of nominals on Γ . Then, we show that this number itself is bounded, completing the termination proof.
We write Γ →R Δ to denote that Δ is obtained from Γ by a single application of the rule R. We write Γ → Δ if there is some R such that Γ →R Δ.
We write SΓ for the set of all modal expressions occurring on Γ , possibly as subterms of other expressions, and Rel Γ for the set of all roles that occur on Γ . Crucial for the termination argument is the fact the the tableau rules cannot introduce any modal expressions that do not already occur on the initial branch. Proposition 7.1. If Γ, Δ are branches such that Δ is obtained from Γ by any rule of T , then SΔ = SΓ .
For every pair of nominals x, y and every role r, a branch Γ may contain an edge rxy, an equation x=y or a disequation x6=. y. For every expression s ∈ SΓ , . Γ may contain a formula sx. Tableau rule application can introduce at most one formula α:[r]ntx for each box expression [r]nt and each nominal x. Finally, a branch may contain ⊥. So, since the initial branch Γ0 contains no formulas of the form α:tx, the size of Γ derived from Γ0 is bounded by |Rel Γ | · |N Γ |2 + 2|N Γ |2 + 2|SΓ | · |N Γ | + 1. By Proposition 7.1, we know that |SΓ | and |Rel Γ | depend only on the initial branch.
By the above, it suffices to show that |N Γ | is bounded in the sum of the sizes of the initial formulas. We do so by giving a bound on the number of applications of R♦ and RE that can occur in the derivation of a branch, which suffices since the two rules are the only ones that can introduce new nominals.
For RE, we do so by defining ψEΓ := {Ens ∈ SΓ | ∃x ∈ N Γ : Ensx not evident on Γ } and showing that |ψEΓ | decreases with every application of RE (and is non-increasing otherwise, which is obvious).
Proposition 7.2. Γ R→E Δ =⇒ |ψEΓ | > |ψEΔ|
The proof proceeds analogously to the corresponding arguments in [
Now we show that R♦ can be applied at most finitely often in a derivation. Since there are only finitely many roles, it suffices to show that R♦ can be applied at most finitely often for each role. Since R♦ is only applicable to diamond formulas that are not quasi-evident, the following holds: Proposition 7.3. If R♦ is applicable to a formula hrinsx ∈ Γ , then either
2. PΓr x is not expanded on Γ .
Let Δ be a branch obtained from some Γ by applying R♦ to a formula hrinsx ∈ Γ such that PΓr x is not expanded on Γ . Clearly, P Δrx must be expanded on Δ.
Since Γ → Δ implies Γ˜ ⊆ Δ˜, it holds: Proposition 7.4. Let s ∈ Γ be a diamond formula and Γ → Δ.
1. PΓr x ⊆ P Δrx. 2. If P is expanded on Γ , then P is expanded on Δ.
Termination of our calculus follows analogously to [
A rule R is said to be applied to a nominal x ∈ N Γ if R is applied to a formula tx ∈ Γ . Given a pattern P , we define AP := {α ∈ P }.
Lemma 7.1. Let Γ0 be an initial branch and Γ0 → Γ1 → . . . a derivation. Let r be a role, A a set of labels, and
I := {i | ∃x : Γi+1 is obtained from Γi by applying R♦ to x ∧ A(PΓri x) = A} Then |I| ≤ |Pat rΓ0| · |{hrimt ∈ SΓ0}|.
Proof. Follows by Propositions 7.1, 7.3, 7.4 and 7.5 as Γ0 contains no edges. An
analogous argument for a similar calculus and A = ∅ is detailed in [
A set of labels A is called a pattern space for a role r on a branch Γ if there is some x ∈ N Γ such that A(PΓr x) = A. By Lemma 7.1, it suffices to show that for each role r, the number of pattern spaces created during a derivation is bounded.
Lemma 7.2. Let Γ0 be an initial branch, r a role and A a set of labels. There is a function f : IN → IN such that, for every derivation Γ0 → Γ1 → . . .: |{x | ∃i, y : i ≥ 0 ∧ A(PΓri x) = A ∧ rxy ∈ Γi}| ≤ f |A| Proof. Let r and Γ0 → Γ1 → . . . be as required. Let XA := {x | ∃i, y : i ≥ 0 ∧ A(PΓri x) = A ∧ rxy ∈ Γi}. We proceed by induction on n := |A|. For every x ∈ XA, let ix be the least i such that 1. A(PΓri x) = A, and 2. for some y, rxy ∈ Γi.
Since Γ0 contains no edges, ix ≥ 1. No single rule application can make 1 and 2 true at the same time. Hence, for every x ∈ XA exactly one of the following is true: Case A(PΓrix−1 x) ( A. Then there is some y such that rxy ∈ Γix−1. So, x ∈ XB for some proper subset B of A. Clearly, this case is only possible if |A| > 0. Case ∄y : rxy ∈ Γix−1. Then A(PΓrix−1x) = A. So, ix − 1 belongs to the set I from Lemma 7.1. This is the only case possible if |A| = 0.
By the above, f can be defined as follows: f 0 := |Pat rΓ0| · |{hrimt ∈ SΓ0}| A label α is said to be generated at level n in a derivation Γ0 → Γ1 → . . . if there is some i ≥ 0 such that α is generated by an application of RT extending Γi by a formula α:[r]mtx, and LΓi(PΓri x) = n.
Lemma 7.3. Let Γ0 → Γ1 → . . . be a derivation where Γ0 is initial and T r ∈ Γ0. Let x ∈ N Γi. Then every α ∈ PΓri x is generated at level strictly less than LΓi(PΓri x).
Proof. Assume, by contradiction, Γi, r, and x are all as required and there is some α ∈ PΓri x such that α is generated at level m ≥ LΓi(PΓri x). Then there is some j < i such that α is generated by an application of RT to some ryz ∈ Γj such that LΓj (PΓrj y) = m. By the applicability restriction on RT (non-subsumption), LΓj+1 (PΓrj+1 y) = m + 1, and therefore LΓi (PΓri y) > m. Since α ∈ PΓri x, by Lemma 6.3 it holds y ⊲rΓi x. Since r is transitive, A(PΓri y) ⊆ A(PΓri x). Consequently, LΓi(PΓri x) ≥ LΓi(PΓri y) > m ≥ LΓi(PΓri x). Contradiction. ⊓⊔
By Lemma 7.3, the number of pattern spaces with level n (i.e., pattern spaces
whose patterns have level n) is bounded from above by 2m, where m is the
number of labels generated at levels less than n. Clearly, the level of r-patterns in
a derivation from Γ0 is bounded by |{[r]kt ∈ SΓ0}|. Also, by the
applicability restriction on RT (non-subsumption), no labels can be generated at level
|{[r]kt ∈ SΓ0}|. Hence, in order to show that the number of pattern spaces
created during a derivation is bounded, it suffices to bound the number of labels
generated at all levels less than |{[r]kt ∈ SΓ0}|. A label α is called r-label (in a
derivation Γ0 → Γ1 → . . .) if there are i, n, t, x such that α:[r]ntx ∈ Γi.
Lemma 7.4. Let Γ0 be an initial branch and T r ∈ Γ0. There is a function
f : IN → IN such that, for every derivation Γ0 → Γ1 → . . . and 0 ≤ n < |{[r]kt ∈
SΓ0}|: |{α | ∃m ≤ n : α is an r-label generated at level m}| ≤ f n.
Proof. We define f by induction on n. Let Am := {α | ∃k ≤ m : α is an r-label
generated at level k}, and Am := ∅ if m < 0. A new label can only be generated
by an application of RT . Therefore, by the applicability condition of RT , |An| ≤
|{[r]mt ∈ SΓ0}| · |{x | ∃i, y : i ≥ 0 ∧ LΓi (PΓri x) ≤ n ∧ rxy ∈ Γi}|. By Lemma 7.3,
|An| ≤ |{[r]mt ∈ SΓ0}| · | SB⊆An−1 {x | ∃i, y : i ≥ 0 ∧ A(PΓri x) = B ∧ rxy ∈
Γi}|. By Lemma 7.2, there is a function g such that |An| ≤ |{[r]mt ∈ SΓ0}| ·
P|kA=n0−1| |An−1| gk ≤ |{[r]mt ∈ SΓ0}| · 2|An−1|g|An−1|. Hence, we can define:
k
f 0 := |{[r]mt ∈ SΓ0}| · g0
f n := |{[r]mt ∈ SΓ0}| · 2f(n−1)g(f (n − 1))
To account for non-local constraints introduced by number restrictions on
transitive roles, the notion of patterns from [
The termination proof establishes a non-elementary complexity bound for the
associated decision procedure. Presently, we do not know if this bound is strict.
Still, we believe that this procedure is well-suited for efficient implementation
despite its potentially high worst-case complexity. In fact, if applied to problems
that do not contain number restrictions on transitive roles, the complexity of the
procedure matches the NExpTime bound of [
While SHQ with number restrictions on transitive roles is, in general,
undecidable [
Acknowledgment. We would like to thank the anonymous referees for their careful reading and helpful suggestions to this paper.