=Paper=
{{Paper
|id=Vol-477/paper-30
|storemode=property
|title=Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles
|pdfUrl=https://ceur-ws.org/Vol-477/paper_41.pdf
|volume=Vol-477
|dblpUrl=https://dblp.org/rec/conf/dlog/KaminskiS09
}}
==Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles==
https://ceur-ws.org/Vol-477/paper_41.pdf
Terminating Tableaux for SOQ with Number
Restrictions on Transitive Roles
Mark Kaminski and Gert Smolka
Saarland University, Saarbrücken, Germany
Abstract. We show that the description logic SOQ with number re-
strictions on transitive roles is decidable by a terminating tableau cal-
culus. 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.
1 Introduction
Efficient tableau algorithms are available for a wide range of description logics,
including logics that contain both transitive roles and functional or number re-
strictions, like SIN [1], SHIF [2, 3], SHIQ [4], SHOQ [5], SHOIQ [6], and
SROIQ [7]. In all cases, however, the language is restricted to contain no num-
ber restrictions on complex roles, e.g., on transitive roles, or roles containing
transitive subroles. Although desirable for applications [8], number restrictions
on complex roles lead to undecidability for logics extending SHIN [3]. In the
absence of inverse roles (I), however, the limitation of number restrictions to
simple roles can be significantly relaxed [8]. In particular, the result in [8] im-
plies the decidability of SQ extended by number restrictions on transitive roles.
Obtained via a small model theorem, this decidability result does not yield prac-
tical decision procedures. Nor does it seem to imply the decidability of extensions
of SQ with nominals.
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 [9] by primitive transitive roles (S), nominals (O), and qualified num-
ber restrictions (Q). We show that reasoning in SOQ+ is decidable by giving a
terminating tableau calculus for concept satisfiability in SOQ+ extended by the
universal role. Having the universal role in the language allows us to internalize
terminological axioms, reducing reasoning with respect to TBoxes to concept
satisfiability [10, 11].
For termination, our calculus employs pattern-based blocking. Pattern-based
blocking is introduced in [12, 13] for converse-free hybrid logic with global modal-
ities. In [14], the technique is extended to graded logics subsuming SOQ and
SHOQ. To provide a complete treatment of number restrictions on transitive
roles, we extend pattern-based blocking further, incorporating ideas [15, 16] used
in tableau systems for propositional dynamic logic and propositional µ-calculus.
2 Preliminaries
Following [12–14], our formal presentation is based on simple type theory. Nota-
tionally, our presentation is based on modal syntax, but can easily be translated
to the traditional DL notation following [11]. We start with two base types B
and I. The interpretation of B is fixed and consists of two truth values. The in-
terpretation of I is a nonempty set whose elements are called individuals. Given
two types σ and τ , the functional type στ is interpreted as the set of all total
functions from the interpretation of σ to that of τ . We write σ1 σ2 σ3 for σ1 (σ2 σ3 ).
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 s1 s2 s3 for (s1 s2 )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:
^ .
DX := x6=y
x,y∈X
x6=y
We use the following constants, which we call modal operators.
¬˙ : (IB)IB ¬p
˙ = λx.¬px
∧˙ : (IB)(IB)IB ˙
p ∧ q = λx. px ∧ qx
∨˙ : (IB)(IB)IB p ∨˙ q = λx. px ∨ qx
V
h in : (IIB)(IB)IB hrin p = λx.∃Y. DY ∧ ( y∈Y rxy ∧ py)
V W
[ ]n : (IIB)(IB)IB [r]n p = λx.∀Y. ( y∈Y rxy) ∧ DY → y∈Y py
V
En : (IB)IB En p = λx.∃Y. DY ∧ y∈Y py
W
An : (IB)IB An p = λx.∀Y. DY → y∈Y py
.
˙ : IIB ẋ = λy.x=y
T : (IIB)B T r = ∀xyz.rxy ∧ ryz → rxz
where |Y | = n + 1 in all equations
To the right of each constant is an equation defining its semantics. Formulas of
the form [r]n tx are called box formulas or boxes, and formulas hrin tx are called
diamond formulas or diamonds. The semantics of boxes and diamonds is defined
following [17–19]. Our language does not contain a dedicated symbol for the
universal role. Instead, we use graded global modalities En and An , which are
semantically equivalent to qualified number restrictions on the universal role.
Formulas of the form T r are called transitivity assertions.
We assume the application of modal operators to have a higher precedence
˙ 2 ẏ ∨˙ p x for
than regular functional application. So, for instance, we write ¬hri
((¬(hri
˙ ˙ p)x.
2 (ẏ))) ∨
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 Branches
For the sake of simplicity, we will define our tableau calculus T on negation
normal modal expressions, i.e., terms of the form:
˙ | ẋ | ¬˙ ẋ | t ∧˙ t | t ∨˙ t | hrin t | [r]n t | En t | An t
t ::= p | ¬p
A branch Γ is a finite set of formulas s of the form
. .
s ::= tx | rxy | T r | x=y | x6=y | ⊥ | α:[r]n tx
where t is a negation normal modal expression. The new form α:[r]n tx 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 hri0 ẏ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 Evidence and Pre-evidence
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 quasi-
evident 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 ∈ Γ ⇒ t1 x ∈ Γ̃ ∧ t2 x ∈ Γ̃
(t1 ∨˙ t2 )x ∈ Γ ⇒ t1 x ∈ Γ̃ ∨ t2 x ∈ Γ̃
hrin tx ∈ Γ ⇒ ∃Y : |Y | = n + 1 ∧ DΓ Y ∧ {rxy, ty | y ∈ Y } ⊆ Γ̃
/ Γ̃ }/∼Γ | ≤ n
[r]n tx ∈ Γ ⇒ |{y | rxy ∈ Γ̃ , ty ∈
En tx ∈ Γ ⇒ ∃Y : |Y | = n + 1 ∧ DΓ Y ∧ {ty | y ∈ Y } ⊆ Γ̃
/ Γ̃ }/∼Γ | ≤ n
An tx ∈ Γ ⇒ |{y | ty ∈
ẋy ∈ Γ ⇒ x ∼Γ y
¬˙ ẋ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 {t1 x, t2 x} ⊆ Γ̃ .
Theorem 4.1 (Model Existence). Evident branches are satisfiable.
Proof. Omitted for space reasons. Proceeds similarly to the argument in [14]. ⊓
⊔
To simplify the treatment of transitivity, we introduce the notion of pre-
evidence. 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]n tx ∈ Γ ⇒ |{y | x ⊲rΓ y, ty ∈
/ Γ̃ }/∼Γ | ≤ n
Pre-evidence of individual formulas is defined analogously to the correspond-
ing 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. ⊓
⊔
5 Tableau Rules
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 S in t. The
notation is extended to sets of terms in the natural way: N Γ := {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
“hrin tx 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 Blocking Conditions and Quasi-evidence
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 [14], the notion of quasi-evidence is based on the following observation.
Let Γ be a branch and x, y be nominals such that
– x has no r-successor on Γ , i.e., there is no z such that rxz ∈ Γ̃ ,
– for every r-diamond or r-box tx ∈ Γ̃ , it holds ty ∈ Γ̃ , and
– all r-diamonds and r-boxes sy ∈ Γ̃ are evident on Γ .
(s ∧˙ t)x (s ∨˙ t)x
R∧˙ R∨˙
sx, tx sx | tx
hrin tx
R♦ . Y fresh, |Y | = n + 1, hrin tx not quasi-evident on Γ
∀y, z ∈ Y, y 6= z : y6=z, rxy, ty
[r]n tx
R . Y ⊆ {y | x ⊲rΓ y}, |Y | = |Y /∼Γ | = n + 1
∃y, z ∈ Y, y 6= z : y =z | ∃y ∈ Y : ty
T r, rxy
RT α fresh, [r]n tx ∈ Γ̃ , [r]n tx not subsumed on Γ
α:[r]n tx
En tx
RE . Y fresh, |Y | = n + 1, En tx not evident on Γ
∀y, z ∈ Y, y 6= z : y6=z, ty
An tx
RA . Y ⊆ N Γ, |Y | = |Y /∼Γ | = n + 1
∃y, z ∈ Y, y 6= z : y =z | ∃y ∈ Y : ty
.
ẋy ¬˙ ẋy ¬px
˙ x6=y
RN . RN̄ . R⊥
¬
˙ px ∈ Γ̃ R⊥
6
.
=
x ∼Γ y
x=y x6=y ⊥ ⊥
Γ is the branch to which a rule is applied. “Y fresh” stands for Y ∩ N Γ = ∅.
“α fresh” stands for ∄t, x : α:tx ∈ Γ
Fig. 1. Tableau rules for T
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 hri0 px 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 tran-
sitive roles, we refine the notion of a pattern and the quasi-evidence conditions
from [14]. Similarly to the usage of “history variables” in [16] in order to track
the propagation of eventuality constraints, we use labels to represent constraints
on the successors of a nominal x that are introduced by r-boxes at x if r is
transitive.
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]n tx ∈ Γ . 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 Γ .
u: [r]1 ¬p
˙ u: [r]1 ¬p
˙
r r r r
x: hri0 p y: hri0 p v: p x: hri0 p, ¬p
˙ y: hri0 p x: hri0 p, ¬p
˙ y: hri0 p, ¬p
˙
r r r r r r
z: p z: p z: p
a) b) r transitive c) r transitive
Fig. 2. Number restrictions and transitivity
A diamond hrin sx ∈ Γ 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 hrin sx ∈ Γ
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:
hrin tx ∈ Γ ⇒ hrin tx is quasi-evident on Γ
T r ∈ Γ ⇒ ∀n, t, x : [r]n tx ∈ Γ̃ ⇒ ∃z, α : z DrΓ x ∧ α:[r]n tz ∈ Γ
α:tx ∈ Γ ⇒ tx ∈ Γ ∧ ∀y : x ⊲rΓ y ⇔ y:Γ α
Lemma 6.1. Let Γ be a branch. Let {[r]n tx, [r]n ty} ⊆ Γ̃ such that T r ∈ Γ and
x DrΓ y. Then: [r]n tx is pre-evident on Γ =⇒ [r]n ty is pre-evident on Γ
Lemma 6.2. Let Γ be a quasi-evident branch. Let hrin sx ∈ Γ 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 : hrim t ∈ PΓr x =⇒ hrim tx is evident on ∆,
3. hrin sx is evident on ∆,
4. ∀r′ , m, t, z : hr′ im tz is evident on Γ =⇒ hr′ im tz 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 hri0 px 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 [14], using Lemma 6.2(3-5). ⊓
⊔
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 pre-
evident or quasi-evident on Γ by induction on the size of s. The quasi-evidence
of formulas α:tx follows by Lemma 6.3. ⊓
⊔
7 Termination
We will now show that every tableau derivation is finite. Since the tableau rules
are all finitely branching, by König’s lemma it suffices to show that the con-
struction 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.
R
We write Γ → ∆ to denote that ∆ is obtained from Γ by a single application
R
of the rule R. We write Γ → ∆ if there is some R such that Γ → ∆.
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]n tx for each box expression [r]n t 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 Γ := {En s ∈ SΓ | ∃x ∈ N Γ : En sx not
evident on Γ } and showing that |ψE Γ | decreases with every application of RE
(and is non-increasing otherwise, which is obvious).
R
Proposition 7.2. Γ →E ∆ =⇒ |ψE Γ | > |ψE ∆|
The proof proceeds analogously to the corresponding arguments in [12, 13].
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 hrin sx ∈ Γ , then either
1. x has an r-successor on Γ , or
2. PΓr x is not expanded on Γ .
Let ∆ be a branch obtained from some Γ by applying R♦ to a formula hrin sx ∈ Γ
such that PΓr x is not expanded on Γ . Clearly, P∆
r
x must be expanded on ∆.
˜
Since Γ → ∆ implies Γ̃ ⊆ ∆, it holds:
Proposition 7.4. Let s ∈ Γ be a diamond formula and Γ → ∆.
1. If s is evident on Γ , then s is evident on ∆.
2. If ∆ is obtained from Γ by applying R♦ to s, then s is evident on ∆.
Proposition 7.5. Let Γ → ∆, x ∈ N Γ , and P be an r-pattern.
1. PΓr x ⊆ P∆r
x.
2. If P is expanded on Γ , then P is expanded on ∆.
Termination of our calculus follows analogously to [14], provided we can, for
each role r, bound the number of applications of R♦ . In the case of [14], this
bound can be given as |Pat r Γ0 | where Γ0 is the initial branch and Pat r Γ :=
P({hrin s ∈ SΓ } ∪ {[r]n s ∈ SΓ }). The present situation is more complex since
now patterns may contain labels in addition to modal expressions. Unlike SΓ0 ,
the set of labels introduced on the branch may grow during tableau construction.
Still, we can bound the number of applications of R♦ for every given set of labels.
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 | · |{hrim t ∈ 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 [14]. ⊓
⊔
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 −1 x) = 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 | · |{hrim t ∈ SΓ0 }|
n−1
X
n
f n := |Pat r Γ0 | · |{hrim t ∈ SΓ0 }| + fk if n > 0 ⊓
⊔
k
k=0
We define the level of an r-pattern P on Γ as:
LΓ P := |{[r]m t ∈ SΓ | ∃α, y : α ∈ P ∧ α:[r]m ty ∈ Γ }|
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]m tx, 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). Conse-
quently, 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 num-
ber of labels generated at levels less than n. Clearly, the level of r-patterns in
a derivation from Γ0 is bounded by |{[r]k t ∈ SΓ0 }|. Also, by the applicabil-
ity restriction on RT (non-subsumption), no labels can be generated at level
|{[r]k t ∈ SΓ0 }|. Hence, in order to show that the number of pattern spaces cre-
ated during a derivation is bounded, it suffices to bound the number of labels
generated at all levels less than |{[r]k t ∈ SΓ0 }|. A label α is called r-label (in a
derivation Γ0 → Γ1 → . . .) if there are i, n, t, x such that α:[r]n tx ∈ Γ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]k t ∈
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]m t ∈ SΓ0 }| · |{x | ∃i, y : Si ≥ 0 ∧ LΓi (PΓri x) ≤ n ∧ rxy ∈ Γi }|. By Lemma 7.3,
|An | ≤ |{[r]m t ∈ SΓ0 }| · | B⊆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]m t ∈ SΓ0 }| ·
P|An−1 | |An−1 |
k=0 k gk ≤ |{[r]m t ∈ SΓ0 }| · 2|An−1 | g|An−1 |. Hence, we can define:
f 0 := |{[r]m t ∈ SΓ0 }| · g0
f n := |{[r]m t ∈ SΓ0 }| · 2f (n−1) g(f (n − 1)) if n > 0 ⊓
⊔
8 Conclusion
To account for non-local constraints introduced by number restrictions on tran-
sitive roles, the notion of patterns from [14] needs to be extended. The extension
is semantically intuitive and allows for a simple proof of model existence. As it
comes to termination, the reasoning in [14] needs to be refined considerably.
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 [14], which is even lower than the
2-NExpTime bound established for practically successful procedures of [2–6].
While SHQ with number restrictions on transitive roles is, in general, unde-
cidable [8], decidability can be regained for SHQ-terminologies satisfying certain
admissibility criteria [8]. We believe that the present algorithm can be extended
to cover terminologies satisfying these criteria.
Acknowledgment. We would like to thank the anonymous referees for their
careful reading and helpful suggestions to this paper.
References
1. Horrocks, I., Sattler, U., Tobies, S.: A PSpace-algorithm for deciding ALCN I R+ -
satisfiability. Technical Report LTCS-98-08, LuFg Theoretische Informatik, RWTH
Aachen, Germany (1998)
2. Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and
role hierarchies. J. Log. Comput. 9(3) (1999) 385–410
3. Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for very expressive descrip-
tion logics. L. J. IGPL 8(3) (2000) 239–263
4. Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for expressive description
logics. In Ganzinger, H., McAllester, D.A., Voronkov, A., eds.: LPAR’99. Volume
1705 of LNCS., Springer (1999) 161–180
5. Horrocks, I., Sattler, U.: Ontology reasoning in the SHOQ(D) description logic. In
Nebel, B., ed.: Proc. 17th Intl. Joint Conf. on Artificial Intelligence (IJCAI 2001),
Morgan Kaufmann (2001) 199–204
6. Horrocks, I., Sattler, U.: A tableau decision procedure for SHOIQ. J. Autom.
Reasoning 39(3) (2007) 249–276
7. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In Do-
herty, P., Mylopoulos, J., Welty, C.A., eds.: Proc. 10th Intl. Conf. on Principles of
Knowledge Representation and Reasoning (KR 2006), AAAI Press (2006) 57–67
8. Kazakov, Y., Sattler, U., Zolin, E.: How many legs do I have? Non-simple roles in
number restrictions revisited. In Dershowitz, N., Voronkov, A., eds.: LPAR 2007.
Volume 4790 of LNCS., Springer (2007) 303–317
9. Schmidt-Schauß, M., Smolka, G.: Attributive concept descriptions with compli-
ments. Artif. Intell. 48(1) (1991) 1–26
10. Baader, F.: Augmenting concept languages by transitive closure of roles: An al-
ternative to terminological cycles. [20] 446–451
11. Schild, K.: A correspondence theory for terminological logics: Preliminary report.
[20] 466–471
12. Kaminski, M., Smolka, G.: Hybrid tableaux for the difference modality. In Areces,
C., Demri, S., eds.: Proc. 5th Workshop on Methods for Modalities (M4M5 2007).
Volume 231 of Electr. Notes Theor. Comput. Sci., Elsevier (2009) 241–257
13. Kaminski, M., Smolka, G.: Terminating tableau systems for hybrid logic with
difference and converse. To appear in J. Log. Lang. Inf. (2009)
14. Kaminski, M., Schneider, S., Smolka, G.: Terminating tableaux for graded hybrid
logic with global modalities and role hierarchies. In: TABLEAUX 2009, Springer
(2009) To appear.
15. Stirling, C., Walker, D.: Local model checking in the modal mu-calculus. Theor.
Comput. Sci. 89(1) (1991) 161–177
16. De Giacomo, G., Massacci, F.: Combining deduction and model checking into
tableaux and algorithms for converse-PDL. Inf. Comput. 162(1–2) (2000) 117–137
17. Fattorosi-Barnaba, M., De Caro, F.: Graded modalities. I. Stud. Log. 44(2) (1985)
197–221
18. van der Hoek, W., de Rijke, M.: Counting objects. J. Log. Comput. 5(3) (1995)
325–345
19. Ohlbach, H.J., Schmidt, R.A., Hustadt, U.: Translating graded modalities into
predicate logic. In Wansing, H., ed.: Proof Theory of Modal Logic. Volume 2 of
Applied Logic Series. Kluwer (1996) 253–291
20. Mylopoulos, J., Reiter, R., eds.: Proc. 12th Intl. Joint Conf. on Artificial Intelli-
gence, Morgan Kaufmann (1991)