<figure><img src="image_1.png" /></figure>

HAL
open science

# Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles

Mark Kaminski, Gert Smolka

<figure><img src="image_2.png" /></figure>

## To cite this version:

Mark Kaminski, Gert Smolka. Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles. 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS) / Held as Part of World Computer Congress (WCC), Sep 2010, Brisbane, Australia. pp.213-228, 10.1007/978-3-642-15240-5_16. hal-01054458

HAL Id: hal-01054458

https://inria.hal.science/hal-01054458

Submitted on 6 Aug 2014

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_3.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# 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 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.

## 1 Introduction

Number restrictions on roles are an expressive feature of description logics that allows to impose counting constraints on the number of objects that are related via a certain role. Qualified number restrictions [6] correspond to graded modalities [4, 3, 5] in modal logics. Transitive roles are prominently used in description logics for representing parthood relationships [21].

Efficient tableau algorithms are available for a wide range of description logics, including logics that contain both transitive roles and number restrictions, such as *SIN* [11], *SHIF* [8, 13], *SHIQ* [12], *SHOQ* [9], *SHOIQ* [10], and *SROIQ* [7]. In all cases, however, the language is restricted to contain no number restrictions on *complex roles*, e.g., on transitive roles, or roles containing transitive subroles. Although desirable for applications [19], number restrictions on complex roles lead to undecidability for logics extending *SHIN* [13]. In the absence of inverse roles (*I*), however, the limitation of number restrictions to simple roles can be significantly relaxed [19]. In particular, the result in [19] implies the decidability of *SQ* extended by number restrictions on transitive roles. Obtained via a small model theorem, this decidability result does not yield practical decision procedures. Nor does it imply the decidability of extensions of *SQ* with nominals.

We consider the logic *SOQ* with number restrictions on transitive roles, and call it *SOQ*<sup>+</sup>. As indicated by its name, *SOQ*<sup>+</sup> extends the basic description logic *ALC* [23] by primitive transitive roles (*S*), nominals (*O*), and qualified number restrictions (*Q*), where we allow such restrictions on transitive roles (+). We show that reasoning in *SOQ*<sup>+</sup> is decidable by giving a terminating tableau calculus for concept satisfiability in *SOQ*<sup>+</sup> 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 [1, 22].

<footnote>* A preliminary version of this work appeared in [17].</footnote>
For termination, our calculus employs *pattern-based blocking*. Pattern-based blocking is introduced in [15, 16] for converse-free hybrid logic with global modalities. 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 [25, 2] used in tableau systems for propositional dynamic logic and propositional μ-calculus.

## 2 Preliminaries

Following [15, 16, 14], our formal presentation is based on simple type theory. Notationally, our presentation is based on modal syntax, but can easily be translated to the traditional DL notation [22]. We start with two base types B and I. The interpretation of B is fixed and consists of the two truth values. The interpretation 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 $s_1s_2s_3$ for $(s_1s_2)s_3$. 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 $x≠y$ for $¬(x= y)$.

Let us write $∃X.s$ for $∃x_1...x_n.s$ if $|X| = n$ and $X = \{x_1, ..., x_n\}$. Also, given a set X of nominals, we use the following abbreviation:

$$DX := \bigwedge_{\substack{x,y \in X \\ x \neq y}} x \neq y$$

We use the following constants, which we call *modal operators*.

$$ \begin{array}{l@{\qquad}l} \dot{\neg}: (\mathbf{I}\mathbf{B})\mathbf{IB} & \dot{\neg}p = \lambda x. \neg px \\ \dot{\wedge}: (\mathbf{I}\mathbf{B})(\mathbf{I}\mathbf{B})\mathbf{IB} & p \dot{\wedge} q = \lambda x. px \wedge qx \\ \dot{\vee}: (\mathbf{I}\mathbf{B})(\mathbf{I}\mathbf{B})\mathbf{IB} & p \dot{\vee} q = \lambda x. px \vee qx \\ \langle\neg\rangle_n: (\mathbf{I}\mathbf{B})(\mathbf{I}\mathbf{B})\mathbf{IB} & \langle r \rangle_n p = \lambda x. \exists Y. DY \wedge (\bigwedge_{y \in Y} rxy \wedge py) \\ \text{[]}_n: (\mathbf{I}\mathbf{B})(\mathbf{I}\mathbf{B})\mathbf{IB} & [r]_n p = \lambda x. \forall Y. (\bigwedge_{y \in Y} rxy) \wedge DY \rightarrow \bigvee_{y \in Y} py \\ E_n: (\mathbf{I}\mathbf{B})\mathbf{IB} & E_n p = \lambda x. \exists Y. DY \wedge \bigwedge_{y \in Y} py \\ A_n: (\mathbf{I}\mathbf{B})\mathbf{IB} & A_n p = \lambda x. \forall Y. DY \rightarrow \bigvee_{y \in Y} py \\ \dot{\cdot}: \mathbf{I}\mathbf{B} & \dot{x} = \lambda y. x \dot{=} y \\ T: (\mathbf{I}\mathbf{B})\mathbf{B} & Tr = \forall xyz.rxy \wedge ryz \rightarrow rxz \end{array} $$

where $n \ge 0$ and $|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 $\langle r \rangle_n tx$ are called diamond formulas or diamonds. The semantics of boxes and diamonds is defined following [3, 5]. Intuitively, it can be described as follows:

- $\langle r \rangle_n p$: There are at least $n+1$ r-successors satisfying $p$.

- $[r]_n p$: All r-successors but possibly n exceptions satisfy $p$.

Our language does not contain a dedicated symbol for the universal role. Instead, we use graded global modalities $E_n$ and $A_n$, which are semantically equivalent to qualified number restrictions on the universal role. So, for instance, $E_1 p$ holds if there are at least two distinct states satisfying $p$. Formulas of the form $Tr$ are called transitivity assertions. We assume the application of modal operators to have a higher precedence than regular functional application. So, for instance, we write $\dot{\neg}\langle r \rangle_2 \dot{y} \dot{v} p x$ for $((\dot{\neg}(\langle r \rangle_2 \dot{y}))) \dot{v} p)x$.

A modal interpretation $\mathfrak{M}$ is an interpretation of simple type theory that interprets $B$ as the set $\{0, 1\}$, $\perp$ as 0 (i.e., false), $\top$ as 1 (i.e., true), maps $I$ to a non-empty set, gives the logical constants $\neg$, $\wedge$, $\vee$, $\rightarrow$, $\exists$, $\forall$, $\doteq$ their usual meaning, and satisfies the equations defining the modal operators $\dot{\neg}$, $\dot{\wedge}$, $\dot{\vee}$, $\langle\neg\rangle_n$, $\neg$-n, $E$, $A$, $\dot{\neg}$ and $T$. If $\mathfrak{M}t = 1$, we say that $\mathfrak{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 $\mathcal{T}$ on negation normal modal expressions, i.e., terms of the form:

$$t ::= p \mid \dot{\neg} p \mid \dot{x} \mid \dot{\neg} \dot{x} \mid t \dot{\wedge} t \mid t \dot{\vee} t \mid \langle r \rangle_n t \mid [r]_n t \mid E_n t \mid A_n t$$

A branch $\Gamma$ is a finite set of formulas $s$ of the form:

$$s ::= tx \mid rxy \mid Tr \mid x \dot{=} y \mid x \dot{\neq} y \mid \perp \mid \alpha: [r]_n tx$$

where $t$ is a negation normal modal expression. The new form $\alpha: [r]_n tx$ serves algorithmic purposes. The label $\alpha$ 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 $\perp$ to explicitly mark unsatisfiable branches. We call a branch $\Gamma$ closed if $\perp \in \Gamma$. Otherwise, $\Gamma$ is called open. An interpretation $\mathfrak{M}$ satisfies a branch $\Gamma$ if $\mathfrak{M}$ satisfies all proper formulas on $\Gamma$, i.e., all formulas except for label introductions. Given a finite set of input formulas (i.e., a branch) $\Gamma_0$, our tableau calculus decides if $\Gamma_0$ is satisfiable. We call $\Gamma_0$ the initial branch. The initial branch 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 $\langle r \rangle_0 \dot{y} x$.

Let $\Gamma$ be a branch. With $\sim_{\Gamma}$ we denote the least equivalence relation $\sim$ on nominals such that $x \sim y$ for every equation $x \dot{=} y \in \Gamma$. We define the equational closure $\tilde{\Gamma}$ of a branch $\Gamma$ as:

$$\tilde{\Gamma} := \Gamma \cup \{tx \mid t \text{ modal expression and } \exists x' : x' \sim_{\Gamma} x \text{ and } tx' \in \Gamma\} \\ \cup \{rxy \mid \exists x', y' : x' \sim_{\Gamma} x \text{ and } y' \sim_{\Gamma} y \text{ and } rx'y' \in \Gamma\}$$
# 4 Evidence and Pre-evidence

The proof of model existence for our calculus $\mathcal{T}$ proceeds in three stages. Applied to a satisfiable initial branch, the rules of $\mathcal{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_\Gamma X$ as an abbreviation for $\forall x, y \in X : x \neq y \Rightarrow x \neq y \in \Gamma$. A branch $\Gamma$ is called evident if it satisfies all of the following evidence conditions:

$$
\begin{align*}
(t_1 \hat{\wedge} t_2)x \in \Gamma &\implies t_1x \in \tilde{\Gamma} \text{ and } t_2x \in \tilde{\Gamma} \\
(t_1 \dot{\wedge} t_2)x \in \Gamma &\implies t_1x \in \tilde{\Gamma} \text{ or } t_2x \in \tilde{\Gamma} \\
\langle r \rangle_n tx \in \Gamma &\implies \exists Y : |Y| = n + 1 \text{ and } D_\Gamma Y \text{ and } \{rxy, ty \mid y \in Y\} \subseteq \tilde{\Gamma} \\
[r]_n tx \in \Gamma &\implies |\{y \mid rxy \in \tilde{\Gamma}, ty \notin \tilde{\Gamma}\} / \sim_r| \le n \\
E_n tx \in \Gamma &\implies \exists Y : |Y| = n + 1 \text{ and } D_\Gamma Y \text{ and } \{ty \mid y \in Y\} \subseteq \tilde{\Gamma} \\
A_n tx \in \Gamma &\implies |\{y \mid ty \notin \tilde{\Gamma}\} / \sim_r| \le n \\
\dot{xy} \in \Gamma &\implies x \sim_{\Gamma} y \\
\dot{xy} \in \Gamma &\implies x \not\sim_{\Gamma} y \\
x \neq y \in \Gamma &\implies x \not\sim_{\Gamma} y \\
\dot{px} \in \Gamma &\implies px \notin \tilde{\Gamma} \\
Tr \in \Gamma &\implies \forall x, y, z : rxy \in \tilde{\Gamma} \text{ and } ryz \in \tilde{\Gamma} \implies rxz \in \tilde{\Gamma}
\end{align*}
$$

A formula $s$ is called evident on $\Gamma$ if $\Gamma$ satisfies the right-hand side of the evidence condition corresponding to $s$. For instance, $(t_1 \hat{\wedge} t_2)x$ is evident on $\Gamma$ if and only if $\{t_1x, t_2x\} \subseteq \tilde{\Gamma}$.

We will now show that evident branches are satisfiable. Given a term $t$, we write $\mathcal{N}t$ for the set of nominals that occur in $t$. The notation is extended to sets of terms in the natural way: $\mathcal{N}\Gamma := \bigcup\{\mathcal{N}t \mid t \in \Gamma\}$.

Given a branch $\Gamma$, we construct the interpretation $\mathfrak{M}^\Gamma$ by taking as the domain of $S$ the nominals on $\Gamma$, and interpreting propositional variables and roles as the smallest sets that are consistent with the respective assertions on $\Gamma$. To satisfy the equality constraints on $\Gamma$, all nominals that are equivalent modulo $\sim_\Gamma$ are mapped to the same fixed representative.

Let $\Gamma$ be a branch and let $x_0 \in \mathcal{N}\Gamma$. Let $\rho$ be a function from finite sets of nominals to nominals such that $\rho X \in X$ whenever $X$ is nonempty. We define the interpretation $\mathfrak{M}^\Gamma$ as follows:

$$
\begin{align*}
\mathfrak{M}^\Gamma S &:= \mathcal{N}\Gamma \\
\mathfrak{M}^\Gamma x &:= \text{if } x \in \mathcal{N}\Gamma \text{ then } \rho\{y \in \mathcal{N}\Gamma \mid y \sim_\Gamma x\} \text{ else } x_0 \\
\mathfrak{M}^\Gamma p &:= \{x \in \mathcal{N}\Gamma \mid px \in \tilde{\Gamma}\} \\
\mathfrak{M}^\Gamma r &:= \{(x, y) \in (\mathcal{N}\Gamma)^2 \mid rxy \in \tilde{\Gamma}\}
\end{align*}
$$

Note that in the last two lines of the definition, we interpret the set notation as a convenient description for the respective characteristic functions.
**Theorem 4.1 (Model Existence).** If $\Gamma$ is an evident branch, then $\mathfrak{M}^\Gamma$ satisfies $\Gamma$.

*Proof.* Let $\Gamma$ be an evident branch. For every $s \in \Gamma$, we show that $\mathfrak{M}^\Gamma$ satisfies $s$ by induction on $s$. The details are straightforward. $\square$

To simplify the treatment of transitivity, we introduce the notion of pre-evidence. We define the relation $\triangleright_{\Gamma}^r$ as the least relation such that:

$$rxy \in \tilde{\Gamma} \implies x \triangleright_{\Gamma}^r y \\ x \triangleright_{\Gamma}^r y \text{ and } y \triangleright_{\Gamma}^r z \text{ and } Tr \in \Gamma \implies x \triangleright_{\Gamma}^r z$$

We write $x \preceq_{\Gamma}^r y$ iff $x \sim_{\Gamma} y$ or $x \triangleright_{\Gamma}^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 \in \Gamma \implies |\{y | x \triangleright_{\Gamma}^r y \text{ and } ty \notin \tilde{\Gamma}\} / \sim_{\Gamma}| \le 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 $\hat{\Gamma}$ of a branch $\Gamma$ be defined as $\Gamma \cup \{rxy | x \triangleright_{\Gamma}^r y\}$.

**Proposition 4.1.** $rxy \in \hat{\Gamma} \iff rxy \in \tilde{\Gamma} \iff x \triangleright_{\Gamma}^r y$

**Theorem 4.2 (Evidence Completion).** $\Gamma$ pre-evident $\implies \hat{\Gamma}$ evident

*Proof.* Since $\hat{\Gamma}$ differs from $\Gamma$ only in that $\hat{\Gamma}$ may contain more edges, and $\Gamma$ is pre-evident, $\hat{\Gamma}$ satisfies all of the evidence conditions but possibly the ones for boxes and transitivity assertions. The evidence condition for transitivity assertions holds in $\hat{\Gamma}$ by Proposition 4.1 since $\triangleright_{\Gamma}^r$ is transitively closed for every $r$ such that $Tr \in \Gamma$. The condition for boxes is immediate by Proposition 4.1. $\square$

# 5 Tableau Rules

The tableau rules of our calculus $\mathcal{T}$ are defined in Fig. 1. In the rules, we write $\exists x \in X : \Gamma(x)$ for $\Gamma(x_1) | \dots | \Gamma(x_n)$, where $X = \{x_1, \dots, x_n\}$ and $\Gamma(x)$ is a set of formulas parametrized by $x$. In case $X = \emptyset$, the notation translates to $\perp$. Dually, we write $\forall x \in X : \Gamma(x)$ for $\Gamma(x_1), \dots, \Gamma(x_n)$ ($X = \{x_1, \dots, x_n\}$). If $X = \emptyset$, the notation stands for the empty set of formulas.

The side condition of $\mathcal{R}_\diamond$ uses the notion of quasi-evidence, which we will introduce in Sect. 6. For now, assume the rule is formulated with the restriction “$\langle r \rangle_n tx$ not evident on $\Gamma$”.

A box formula $[r]_n tx$ is subsumed on $\Gamma$ if there is a nominal $y$ and a label $\alpha$ such that $y \preceq_{\Gamma}^r x$ and $\alpha: [r]_n ty \in \Gamma$. The rule $\mathcal{R}_T$ is constrained to be applicable
$$ \mathcal{R}_{\wedge} \frac{(s \hat{\Lambda} t)x}{sx, tx} $$

$$ \mathcal{R}_{\vee} \frac{(s \hat{\nabla} t)x}{sx \mid tx} $$

$$ \mathcal{R}_{\diamond} \frac{\langle r \rangle_n tx}{\forall y \in Y: rxy, ty, \forall z \in Y, y \neq z: y \neq z} \quad \begin{array}{l} \text{Y fresh, } |Y| = n+1, \\ \langle r \rangle_n tx \text{ not quasi-evident on } \Gamma \end{array} $$

$$ \mathcal{R}_{\square} \frac{[r]_n tx}{\exists y, z \in Y, y \neq z: y \doteq z \mid \exists y \in Y: ty} \quad Y \subseteq \{y \mid x \triangleright_{\Gamma}^{r} y\}, \quad |Y| = |Y/\sim_{\Gamma}| = n+1 $$

$$ \mathcal{R}_T \frac{Tr, rxy}{\alpha: [r]_n tx} \quad \alpha \text{ fresh, } [r]_n tx \in \tilde{\Gamma}, [r]_n tx \text{ not subsumed on } \Gamma $$

$$ \mathcal{R}_E \frac{E_n tx}{\forall y \in Y: ty, \forall z \in Y, y \neq z: y \neq z} \quad \text{Y fresh, } |Y| = n+1, E_n tx \text{ not evident on } \Gamma $$

$$ \mathcal{R}_A \frac{A_n tx}{\exists y, z \in Y, y \neq z: y \doteq z \mid \exists y \in Y: ty} \quad Y \subseteq \mathcal{N}\Gamma, \quad |Y| = |Y/\sim_{\Gamma}| = n+1 $$

$$ \mathcal{R}_N \frac{\dot{x}y}{x \doteq y} $$

$$ \mathcal{R}_{\tilde{N}} \frac{\dot{x}\dot{y}}{x \neq y} $$

$$ \mathcal{R}_{\perp}^{\perp} \frac{\dot{p}x}{\perp} \quad px \in \tilde{\Gamma} $$

$$ \mathcal{R}_{\neq \perp}^{\perp} \frac{x \neq y}{\perp} \quad x \sim_{\Gamma} y $$

$\Gamma$ is the branch to which a rule is applied. “Y fresh” stands for $Y \cap \mathcal{N}\Gamma = \emptyset$. “$\alpha$ fresh” stands for $\exists t, x: \alpha:tx \in \Gamma$

<caption>Fig. 1. Tableau rules for $\mathcal{T}$</caption>

only to boxes that are not subsumed on $\Gamma$. This ensures, in particular, that $\mathcal{R}_T$ is applied at most once to each individual box formula on the branch.

A branch $\Delta$ is called a proper extension of a branch $\Gamma$ if $\Delta \supseteq \Gamma$ and $\tilde{\Delta} \supsetneq \tilde{\Gamma}$. Note that if $\Delta$ is a proper extension of $\Gamma$, then in particular it holds $\Delta \supsetneq \Gamma$. The converse does not hold: Let $\Gamma := \{\dot{xy}, x \doteq z, z \doteq y\}$ and $\Delta := \Gamma \cup \{x \doteq y\}$. Then $\Delta \supsetneq \Gamma$ but $\Delta$ is not a proper extension of $\Gamma$. We implicitly restrict the applicability of the tableau rules so that a rule $\mathcal{R}$ is only applicable to a formula $s \in \Gamma$ if all of the alternative branches $\Delta_1, \dots, \Delta_n$ resulting from this application are proper extensions of $\Gamma$.

**Proposition 5.1 (Soundness).** Let $\Delta_1, \dots, \Delta_n$ be the branches obtained from a branch $\Gamma$ by a rule of $\mathcal{T}$. Then $\Gamma$ is satisfiable if and only if there is some $i \in \{1, \dots, n\}$ such that $\Delta_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. Consider $\Gamma_0 := \{A_0 \langle r \rangle_0 px\}$. An
application of $\mathcal{R}_A$ to $\Gamma_0$ yields $\Gamma_1 := \Gamma_0 \cup \{\langle r \rangle_0 px\}$, which can be extended by $\mathcal{R}_\diamond$ to $\Gamma_2 := \Gamma_1 \cup \{rxy, py\}$. Now $\mathcal{R}_A$ is applicable again and yields $\Gamma_3 := \Gamma_2 \cup \{\langle r \rangle_0 py\}$, which in turn can be extended by $\mathcal{R}_\diamond$, and so ad infinitum.

To obtain a terminating calculus, we restrict the rule $\mathcal{R}_\diamond$ by weakening the notion of pre-evidence for diamond formulas. The weaker notion, called quasi-evidence, is then used in the side condition of $\mathcal{R}_\diamond$ 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 $\Gamma$ is a labelled graph with the nodes $\mathcal{N}\Gamma$ and edges $\{(x, y) \mid \exists x: rxy \in \Gamma\}$, where a node $x$ is labelled with all expressions $t$ such that $tx \in \Gamma$, and an edge $(x, y)$ is labelled with all roles $r$ such that $rxy \in \Gamma$. A branch can always be represented graphically through its edge graph.

<figure><img src="image_4.png" /><figcaption>**Fig. 2.** Number restrictions and transitivity</figcaption></figure>

In [14], the notion of quasi-evidence is based on the following observation. Let $\Gamma$ be a branch and $x, y$ be nominals such that: (1) $x$ has no $r$-successor on $\Gamma$, i.e., there is no $z$ such that $rxz \in \tilde{\Gamma}$, (2) for every $r$-diamond or $r$-box $tx \in \tilde{\Gamma}$, it holds $ty \in \tilde{\Gamma}$, and (3) all $r$-diamonds and $r$-boxes $sy \in \tilde{\Gamma}$ are evident on $\Gamma$. Then all $r$-diamonds and $r$-boxes $sx \in \tilde{\Gamma}$ can be made evident by extending $\Gamma$ with $\{rxz | ryz \in \tilde{\Gamma}\}$. As an example, consider the edge graph in Fig. 2(a). There, the formula $\langle r \rangle_0 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 $\Gamma$ by an edge $rxz$ may destroy the evidence of $r$-boxes $tu$ such that $u \succ_r^t x$ (Fig. 2(b)). Note, however, that adding an edge $rxz$ cannot destroy the evidence of a box $tu$ such that $u \succ_r^t x$ if we already have $u \succ_r^t 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 [14]. When blocking a nominal $x$ we have to make sure not to violate any graded boxes at the predecessors of $x$. To track the relevant boxes we tag them with labels.

Given a role $r$, an $r$-pattern is a set consisting of modal expressions of the form $\mu t$, where $\mu \in \{\langle r \rangle_n, [r]_n | n \in \mathbb{N}\}$, and labels $\alpha$, such that, for some $n, t, x$: $\alpha: [r]_n tx \in \Gamma$ (although not required by the definition, in all cases where patterns
play a role for termination they will contain at least one diamond). We define:

$$x:\Gamma\alpha \iff \exists r, n, t, y : \alpha:[r]_n ty \in \Gamma \text{ and } y \triangleright_{\Gamma}^r x$$

We write $P_{\Gamma}^r x$ for the largest $r$-pattern $P$ such that $P \subseteq \{\mu t | \mu tx \in \tilde{\Gamma}\} \cup \{\alpha | x:\Gamma\alpha\}$. We call $P_{\Gamma}^r x$ the $r$-pattern of $x$ on $\Gamma$. Looking back at Fig. 2 (b), we have $P_{\Gamma}^r x = \{\langle r \rangle_0 p\}$, $P_{\Gamma}^r u = \{[r]_1 \dot{\to} p\}$, and $P_{\Gamma}^{r'} x = \emptyset$ for all $r' \neq r$. An $r$-pattern $P$ is expanded on $\Gamma$ if there are nominals $x, y$ such that $rxy \in \Gamma$ and $P \subseteq P_{\Gamma}^r x$. In this case, we say that the nominal $x$ expands $P$ on $\Gamma$.

A diamond $\langle r \rangle_n sx \in \Gamma$ is quasi-evident on $\Gamma$ if it is either evident on $\Gamma$ or $x$ has no $r$-successor on $\Gamma$ and $P_{\Gamma}^r x$ is expanded on $\Gamma$. The rule $\mathcal{R}_{\diamond}$ can only be applied to diamonds that are not quasi-evident. Note that whenever $\langle r \rangle_n sx \in \Gamma$ is quasi-evident but not evident (on $\Gamma$), there is a nominal $y$ that expands $P_{\Gamma}^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:

$$\langle r \rangle_n tx \in \Gamma \implies \langle r \rangle_n tx \text{ is quasi-evident on } \Gamma$$

$$Tr \in \Gamma \implies \forall n, t, x: [r]_n tx \in \tilde{\Gamma} \implies \exists z, \alpha: z \triangleright_{\Gamma}^r x \text{ and } \alpha:[r]_n tz \in \Gamma$$

$$\alpha:[r]_n tx \in \Gamma \implies [r]_n tx \in \tilde{\Gamma} \text{ and } \exists y: rxy \in \Gamma \text{ and } \forall s, z: \alpha:sz \in \Gamma \implies s=[r]_n t$$

**Proposition 6.1.** If $\Gamma$ satisfies the quasi-evidence condition for label introductions and $\alpha:[r]_n tx \in \Gamma$, then for all $y, x \triangleright_{\Gamma}^r y \iff y:\Gamma\alpha$.

**Lemma 6.1.** Let $\Gamma$ be a branch. Let $\{[r]_n tx, [r]_n ty\} \subseteq \tilde{\Gamma}$ such that $Tr \in \Gamma$ and $x \triangleright_{\Gamma}^r y$. Then: $[r]_n tx$ is pre-evident on $\Gamma \implies [r]_n ty$ is pre-evident on $\Gamma$.

*Proof.* Let $\Gamma$ be a branch such that $\{[r]_n tx, [r]_n ty\} \subseteq \tilde{\Gamma}$, $Tr \in \Gamma$ and $x \triangleright_{\Gamma}^r y$. Because $\triangleright_{\Gamma}^r$ is transitively closed, we have $x \triangleright_{\Gamma}^r z$ whenever $y \triangleright_{\Gamma}^r z$. The claim follows. $\square$

**Lemma 6.2.** Let $\Gamma$ be a quasi-evident branch. Let $\langle r \rangle_n sx \in \Gamma$ be not evident on $\Gamma$, $y$ be a nominal that expands $P_{\Gamma}^r x$ on $\Gamma$, and $\Delta := \Gamma \cup \{rxz | ryz \in \tilde{\Gamma}\}$. Then:

1. $\forall z: rxz \in \tilde{\Delta} \iff ryz \in \tilde{\Gamma}$ and $x \triangleright_{\Delta}^r z \iff y \triangleright_{\Gamma}^r z$,

2. $\forall m, t: \langle r \rangle_m t \in P_{\Gamma}^r x \implies \langle r \rangle_m tx$ is evident on $\Delta$,

3. $\langle r \rangle_n sx$ is evident on $\Delta$,

4. $\forall r', m, t, z: \langle r' \rangle_m tz$ is evident on $\Gamma \implies \langle r' \rangle_m tz$ is evident on $\Delta$,

5. $\Delta$ is quasi-evident.

*Proof.* We begin with (1). Let $z$ be a nominal. We only show $rxz \in \tilde{\Delta} \iff ryz \in \tilde{\Gamma}$. The other claim follows by induction on the construction of $\triangleright_{\Gamma}^r$ and $\triangleright_{\Delta}^r$. By construction, it holds $ryz \in \tilde{\Gamma} \implies rxz \in \Delta$. The converse implication holds by the fact that $\langle r \rangle_n sx$ is quasi-evident but not evident on $\Gamma$, meaning that $x$ has no $r$-successor on $\Gamma$. It remains to show: $rxz \in \Delta \iff rxz \in \tilde{\Delta}$. The direction from left to right is obvious. For the other direction, assume $rxz \in \tilde{\Delta}$. Then there are $x', z'$ such that $x' \sim_{\Gamma} x$, $z' \sim_{\Gamma} z$, and $rx'z' \in \Delta$. Since $x$ has no $r$-successor
on $\Gamma$, neither does $x'$. Hence, since $rx'z' \in \Delta - \Gamma$, we must have $x' = x$, and so $rxz' \in \Delta$. But then $ryz' \in \tilde{\Gamma}$, and consequently, $ryz \in \tilde{\Gamma}$. The claim follows by the definition of $\Delta$.

Now to (2). Let $\langle r \rangle_m t \in P_{\Gamma}^r x$. Since $P_{\Gamma}^r y \supseteq P_{\Gamma}^r x$, in particular it holds $\langle r \rangle_m ty \in \tilde{\Gamma}$, i.e., there is some $y' \sim_{\Gamma} y$ such that $\langle r \rangle_m ty' \in \Gamma$. By (1), it suffices to show that $\langle r \rangle_m ty$ is evident on $\Gamma$. This is the case since $\langle r \rangle_m ty'$ is quasi-evident on $\Gamma$ (as $\Gamma$ is quasi-evident) and $y'$ has an $r$-successor on $\Gamma$ (as $y$ has one on $\Gamma$).

Claim (3) immediately follows from (2), and (4) is obvious as the evidence of diamonds on a branch cannot be destroyed by adding edges.

Now to (5). Note that the quasi-evidence condition for transitivity assertions holds in $\Delta$ as $\supseteq_{\Gamma}^{r} \subseteq_{\Delta}^{r}$. The quasi-evidence of diamonds $\langle r \rangle_m tx \in \Delta$ holds by (2). So, the only conditions that might in principle be violated in $\Delta$ are:

a) the pre-evidence condition for boxes $[r]_m tx \in \tilde{\Delta}$ and

b) the pre-evidence condition for boxes $[r]_m tz \in \Delta$ such that $z \succcurlyeq_{\Delta}^r x$, if $Tr \in \Gamma$. For (a), it holds $[r]_m ty \in \tilde{\Gamma}$ as $P_{\tilde{\Gamma}}^r y \supseteq P_{\tilde{\Gamma}}^r x = P_{\tilde{\Delta}}^r x$. Hence by (1) it suffices to show that $[r]_m ty$ is pre-evident on $\Gamma$, which is the case since $\Gamma$ is quasi-evident. For (b), by the quasi-evidence condition for transitivity assertions, there is a nominal $u$ and a label $\alpha$ such that $u \supseteq_{\Gamma}^{r} z$ and $\alpha: [r]_m tu \in \Gamma$. Since $Tr \in \Gamma$, $u \supseteq_{\tilde{\Gamma}}^{r} z$ and $z \succcurlyeq_{\Delta}^r x$, it holds $u \succcurlyeq_{\tilde{\Gamma}}^{r} x$. Then $x: \Gamma \alpha$ and, by the quasi-evidence condition for label introductions, $[r]_m tu \in \tilde{\Gamma}$. By Lemma 6.1, it suffices to show that $[r]_m tu$ is pre-evident on $\Delta$. Since $P_{\tilde{\Gamma}}^r y \supseteq P_{\tilde{\Gamma}}^r x$, we have $y: \Gamma \alpha$ and hence $u \succcurlyeq_{\tilde{\Gamma}}^{r} y$ (Proposition 6.1). So, by (1), $x \succcurlyeq_{\Delta}^{r} v$ implies $u \succcurlyeq_{\tilde{\Gamma}}^{r} v$ for all nominals $v$, and consequently, $\forall v : u \succcurlyeq_{\Delta}^{r} v \Leftrightarrow u \succcurlyeq_{\tilde{\Gamma}}^{r} v$. The claim follows since $[r]_m tu$ is pre-evident on $\Gamma$. $\square$

For an illustration of Lemma 6.2, let the edge graph in Fig. 2(a) (without the dashed arrow) represent $\Gamma$. Then $\langle r \rangle_0 px$ is quasi-evident but not evident on $\Gamma$, and $y$ expands $P_{\Gamma}^r x$. The graph with the dashed arrow added corresponds to the branch $\Delta$ in the lemma. The five claims for $\Gamma$ and $\Delta$ are easy to verify.

**Theorem 6.1 (Pre-evidence Completion).** For every quasi-evident branch $\Gamma$ there is a pre-evident branch $\Delta$ such that $\Gamma \subseteq \Delta$.

*Proof.* For every branch $\Gamma$, we define: $\varphi\Gamma := |\{\langle r \rangle_n sx \mid \langle r \rangle_n sx \in \Gamma \text{ and } \langle r \rangle_n sx \text{ is not evident on } \Gamma\}|$. Let $\Gamma$ be quasi-evident. We proceed by induction on $\varphi\Gamma$. If $\varphi\Gamma = 0$, then $\Gamma$ is pre-evident and we are done. Otherwise, there is a diamond $\langle r \rangle_n sx \in \Gamma$ that is not pre-evident on $\Gamma$. Let $y$ be a nominal that expands $P_{\Gamma}^r x$ on $\Gamma$, and let $\Gamma' := \Gamma \cup \{rxz \mid ryz \in \tilde{\Gamma}\}$. By Lemma 6.2(3-5), $\Gamma'$ is quasi-evident and $\varphi\Gamma' < \varphi\Gamma$. So, by the inductive hypothesis, there is some pre-evident branch $\Delta$ such that $\Delta \supseteq \Gamma' \supseteq \Gamma$. $\square$

We write $\Gamma \xrightarrow{\mathcal{R}} \Delta$ to denote that $\Delta$ is obtained from $\Gamma$ by a single application of the rule $\mathcal{R}$. We write $\Gamma \to \Delta$ if there is some $\mathcal{R}$ such that $\Gamma \xrightarrow{\mathcal{R}} \Delta$. A branch is called maximal if it cannot be extended by any tableau rule.

**Lemma 6.3.** Let $\Gamma$ be a branch that is obtained from an initial branch. Then $\Gamma$ satisfies the quasi-evidence condition for label introductions.
*Proof.* Let $\Gamma_0 \to \dots \to \Gamma_n$ be a derivation such that $\Gamma_0$ is an initial branch and $\Gamma_n = \Gamma$. The claim is shown by induction on $n$. Note that the claim is trivial for $n=0$ since initial branches must contain no edges or label introductions. $\square$

In conjunction with Theorems 4.1, 4.2 and 6.1, the following theorem shows
that open maximal branches are satisfiable. Taken together with the termination
argument in Section 7, this establishes the completeness of our calculus.

**Theorem 6.2 (Quasi-evidence).** Every open and maximal branch obtained in
$\mathcal{T}$ from an initial branch is quasi-evident.

*Proof.* Let $\Gamma$ be an open and maximal branch obtained from an initial branch. We show that every $s \in \Gamma$ that is not of the form $px$, $rxy$ or $x \doteq y$ is either pre-evident or quasi-evident on $\Gamma$ by induction on the size of $s$. Quasi-evidence for label introductions follows by Lemma 6.3. $\square$

# 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 $\Gamma$ is bounded by a function in the number of nominals on $\Gamma$. Then,
we show that this number itself is bounded, completing the termination proof.

We write $\mathcal{S}\Gamma$ for the set of all modal expressions occurring on $\Gamma$, possibly
as subterms of other expressions, and $\mathrm{Rel}\,\Gamma$ for the set of all roles that occur
on $\Gamma$. Crucial for the termination argument is the fact the tableau rules cannot
introduce any modal expressions that do not already occur on the initial branch.

**Proposition 7.1.** If $\Gamma, \Delta$ are branches such that $\Delta$ is obtained from $\Gamma$ by any rule of $\mathcal{T}$, then $\mathcal{S}\Delta = \mathcal{S}\Gamma$.

For every pair of nominals $x, y$ and every role $r$, a branch $\Gamma$ may contain an
edge $rxy$, an equation $x \doteq y$ or a disequation $x \not\doteq y$. For every expression $s \in \mathcal{S}\Gamma$, $\Gamma$
may contain a formula $sx$. The tableau rules can introduce at most one formula
$\alpha: [r]_n t x$ for each box expression $[r]_n t$ and each nominal $x$. Finally, a branch may
contain $\perp$. So, since the initial branch $\Gamma_0$ contains no formulas of the form $\alpha:tx$,
the size of $\Gamma$ derived from $\Gamma_0$ is bounded by $|\mathrm{Rel}\,\Gamma| \cdot |\mathcal{N}\Gamma|^2 + 2|\mathcal{N}\Gamma|^2 + 2|\mathcal{S}\Gamma| \cdot$
$|\mathcal{N}\Gamma| + 1$. By Proposition 7.1, we know that $|\mathcal{S}\Gamma|$ and $|\mathrm{Rel}\,\Gamma|$ depend only on $\Gamma_0$.

By the above, it suffices to show that $|\mathcal{N}\Gamma|$ is bounded in the sum of the
sizes of the input formulas (of which there are only finitely many). We do so by
giving a bound on the number of applications of $\mathcal{R}_{\diamond}$ and $\mathcal{R}_E$ 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 $\mathcal{R}_E$, we do so by defining $\psi_{E\Gamma} := \{E_n s \in \mathcal{S}\Gamma \mid \exists x \in \mathcal{N}\Gamma : E_n s x \text{ is not}$
$\text{evident on } \Gamma\}$ and showing that $|\psi_{E\Gamma}|$ decreases with every application of $\mathcal{R}_E$
(and is non-increasing otherwise, which is obvious).
**Proposition 7.2.** $\Gamma \xrightarrow{\mathcal{R}_E} \Delta \implies |\psi_E \Gamma| > |\psi_E \Delta|$

The proof proceeds analogously to the corresponding arguments in [15, 16].

Now we show that $\mathcal{R}_{\diamond}$ can be applied only finitely often. Since $\mathrm{Rel} \Gamma$ is bounded, it suffices to show that $\mathcal{R}_{\diamond}$ can be applied only finitely often for each role. Since $\mathcal{R}_{\diamond}$ is only applicable to diamonds that are not quasi-evident, we have:

**Proposition 7.3.** If $\mathcal{R}_{\diamond}$ is applicable to a formula $\langle r \rangle_n s x \in \Gamma$, then either

1. $x$ has an $r$-successor on $\Gamma$, or

2. $P_{\Gamma}^r x$ is not expanded on $\Gamma$.

Since $\Gamma \to \Delta$ implies $\tilde{\Gamma} \subseteq \tilde{\Delta}$, it holds:

**Proposition 7.4.** Let $s \in \Gamma$ be a diamond formula and $\Gamma \to \Delta$.

1. If $s$ is evident on $\Gamma$, then $s$ is evident on $\Delta$.

2. If $\Delta$ is obtained from $\Gamma$ by applying $\mathcal{R}_{\diamond}$ to $s$, then $s$ is evident on $\Delta$.

**Proposition 7.5.** Let $\Gamma \to \Delta$, $x \in \mathcal{N}\Gamma$, and $P$ be an $r$-pattern.

1. $P_{\Gamma}^r x \subseteq P_{\Delta}^r x$.

2. If $P$ is expanded on $\Gamma$, then $P$ is expanded on $\Delta$.

In the case of [14], the bound on the number of applications of $\mathcal{R}_{\diamond}$ for each role $r$ can be given as $|\mathrm{Pat}^r \Gamma_0|$ where $\Gamma_0$ is the initial branch and $\mathrm{Pat}^r \Gamma := \mathcal{P}(\{\langle r \rangle_n s | \langle r \rangle_n s \in \mathcal{S}\Gamma\} \cup \{[r]_n s | [r]_n s \in \mathcal{S}\Gamma\})$. The present situation is more complex since now patterns may contain labels in addition to modal expressions. Unlike $\mathcal{S}\Gamma$, the set of labels on the branch may grow during tableau construction. Still, we can bound the number of applications of $\mathcal{R}_{\diamond}$ for every given set of labels.

A rule $\mathcal{R}$ is said to be applied to a nominal $x \in \mathcal{N}\Gamma$ if $\mathcal{R}$ is applied to a formula $tx \in \Gamma$. Given a pattern $P$, we define $\mathcal{A}P := \{\alpha | \alpha \in P\}$. Let $N_{\langle r \rangle}^{\Gamma_0}$ be the number of distinct $r$-diamonds occurring on $\Gamma_0$: $N_{\langle r \rangle}^{\Gamma_0} := |\{\langle r \rangle_k t | \langle r \rangle_k t \in \mathcal{S}\Gamma_0\}|$. Let $\Delta$ be obtained from $\Gamma$ by applying $\mathcal{R}_{\diamond}$ to a formula $\langle r \rangle_n s x \in \Gamma$ such that $P_{\Gamma}^r x$ is not expanded on $\Gamma$. Clearly, $P_{\Delta}^r x$ must be expanded on $\Delta$. Hence, let us call such an application of $\mathcal{R}_{\diamond}$ *pattern-expanding*.

**Lemma 7.1.** Let $\Gamma_0$ be an initial branch and $\Gamma_0 \to \Gamma_1 \to \dots$ a derivation. Let $r$ be a role, $A$ a set of labels, and

$$ I_A^r := \{i \mid \exists x : \Gamma_{i+1} \text{ is obtained from } \Gamma_i \text{ by applying } \mathcal{R}_{\diamond} \text{ to } x \text{ and } \mathcal{A}(P_{\Gamma_i}^r x) = A\} $$
Then $|I_A^r| \le 2^{|A|} \cdot |\mathrm{Pat}^r \Gamma_0| \cdot N_{\langle r \rangle}^{\Gamma_0}$.

*Proof.* Let $\Gamma_0 \to \Gamma_1 \to \dots$ be a derivation, $r$ a role and $A$ a set of labels. We begin with two observations:

1. For every set $B$ of labels, there are at most $|\mathrm{Pat}^r \Gamma_0|$ distinct patterns $P$ such that $\mathcal{A}P = B$. Hence, by Proposition 7.5 (2), for every $B$ there are at most $|\mathrm{Pat}^r \Gamma_0|$ pattern-expanding applications of $\mathcal{R}_{\diamond}$ in the entire derivation,
i.e., at most $|\mathrm{Pat}^r \Gamma_0|$ indices $i \in I_B^r$ such that the application of $\mathcal{R}_\diamond$ to $\Gamma_i$ is pattern-expanding. Let us denote the set of such indices by $J_B^r$.

2. By Propositions 7.4 and 7.5 (2), every pattern-expanding application of $\mathcal{R}_\diamond$ to a nominal $x$ is followed by at most $N_{\langle r \rangle}^{\Gamma_0} - 1$ applications of $\mathcal{R}_\diamond$ to nominals that are equivalent to $x$ at the time of the respective application (clearly, none of these following applications is pattern-expanding).

By definition, every index in $I_A^r$ corresponds to an application of $\mathcal{R}_\diamond$. Let $i \in I_A^r$ and let $x$ be the nominal to which $\mathcal{R}_\diamond$ is applied on $\Gamma_i$. By Proposition 7.3, either the application is pattern-expanding or $x$ already has a successor on $\Gamma_i$. In the latter case, the application must be preceded by a pattern-expanding application of $\mathcal{R}_\diamond$ to some nominal $y$ that is equivalent to $x$ ($x \sim_{\Gamma_i} y$). As for the index $j$ corresponding to this preceding application, by Proposition 7.5 (1), we must have $j \in J_B^r$ for some $B \subseteq A$. By the above two observations, we obtain:

$$ 
\begin{aligned}
|I_A^r| &\le |J_A^r| + \sum_{B \subseteq A} |J_B^r| \cdot (N_{\langle r \rangle}^{\Gamma_0} - 1) \\
&\le |\mathrm{Pat}^r \Gamma_0| + 2^{|A|} \cdot |\mathrm{Pat}^r \Gamma_0| \cdot (N_{\langle r \rangle}^{\Gamma_0} - 1) \le 2^{|A|} \cdot |\mathrm{Pat}^r \Gamma_0| \cdot N_{\langle r \rangle}^{\Gamma_0}
\end{aligned}
\quad \square
$$

A set of labels $A$ is called a *pattern space* for a role $r$ on a branch $\Gamma$ if there is some $x \in \mathcal{N}\Gamma$ such that $\mathcal{A}(P_{\Gamma_i}^r x) = A$. By Lemma 7.1, it suffices to show that for each role $r$, the number of pattern spaces created in a derivation is bounded.

**Lemma 7.2.** Let $\Gamma_0$ be an initial branch, $r$ a role and $A$ a set of labels. There is a function $f: \mathbb{N} \to \mathbb{N}$ such that, for every derivation $\Gamma_0 \to \Gamma_1 \to \dots$:

$$ |\{x \mid \exists i, y: i \ge 0 \text{ and } \mathcal{A}(P_{\Gamma_i}^r x) = A \text{ and } rxy \in \Gamma_i\}| \le f(|A|) $$

*Proof.* Let $r$ and $\Gamma_0 \to \Gamma_1 \to \dots$ be as required. Let $X_A := \{x \mid \exists i, y: i \ge 0 \text{ and } \mathcal{A}(P_{\Gamma_i}^r x) = A \text{ and } rxy \in \Gamma_i\}$. We proceed by induction on $n := |A|$. For every $x \in X_A$, let $i_x$ be the least $i$ such that

1. $\mathcal{A}(P_{\Gamma_i}^r x) = A$, and

2. for some $y, rxy \in \Gamma_i$.

Since $\Gamma_0$ is an initial branch, it contains no edges, and so $i_x \ge 1$. No single rule application can make 1 and 2 true at the same time. Hence, for every $x \in X_A$ exactly one of the following is true:

**Case** $\mathcal{A}(P_{\Gamma_{i_x-1}}^r x) \subsetneq A$. Then there is some $y$ such that $rxy \in \Gamma_{i_x-1}$. So, $x \in X_B$ for some proper subset $B$ of $A$. Clearly, this case is only possible if $|A| > 0$.

**Case** $\mathcal{A}(P_{\Gamma_{i_x-1}}^r x) = A$. So, $i_x - 1$ belongs to the set $I_A^r$ from Lemma 7.1. This is the only case possible if $|A| = 0$.

By the above, $f$ can be defined as follows:

$$ 
\begin{aligned}
f_0 &:= |\mathrm{Pat}^r \Gamma_0| \cdot N_{\langle r \rangle}^{\Gamma_0} \\
fn &:= 2^n \cdot |\mathrm{Pat}^r \Gamma_0| \cdot N_{\langle r \rangle}^{\Gamma_0} + \sum_{k=0}^{n-1} \binom{n}{k} \cdot fk \quad \text{if } n > 0
\end{aligned}
\quad \square
$$
We define the level of an r-pattern P on Γ as:

$$L_{\Gamma}P := |\{[r]_m t \in \mathcal{S}\Gamma \mid \exists \alpha, y : \alpha \in P \text{ and } \alpha:[r]_m ty \in \Gamma\}|$$

A label α is said to be generated at level n in a derivation Γ₀ → Γ₁ → ... if there is some i ≥ 0 such that α is generated by an application of R_T extending Γᵢ by a formula α:[r]ₘtx, and L<sub>Γᵢ</sub>(P<sub>Γᵢ</sub><sup>r</sup>x) = n.

**Lemma 7.3.** Let Γ₀ → Γ₁ → ... be a derivation where Γ₀ is initial and Tr ∈ Γ₀. Let x ∈ NΓᵢ. Then every label α ∈ P<sub>Γᵢ</sub><sup>r</sup>x is generated at level strictly less than L<sub>Γᵢ</sub>(P<sub>Γᵢ</sub><sup>r</sup>x).

*Proof.* Assume, by contradiction, Γᵢ, r, and x are all as required and there is some α ∈ P<sub>Γᵢ</sub><sup>r</sup>x such that α is generated at level m ≥ L<sub>Γᵢ</sub>(P<sub>Γᵢ</sub><sup>r</sup>x). Then there is some j < i such that α is generated by an application of R_T to some ryz ∈ Γⱼ such that y ▷<sub>Γᵢ</sub><sup>r</sup> x and L<sub>Γⱼ</sub>(P<sub>Γⱼ</sub><sup>r</sup>y) = m. Then A(P<sub>Γⱼ</sub><sup>r</sup>y) ∪ {α} ⊆ A(P<sub>Γₖ</sub><sup>r</sup>x') and hence (by the applicability restriction on R_T) L<sub>Γₖ</sub>(P<sub>Γₖ</sub><sup>r</sup>x') > m holds for all k ≥ j + 1 and all x' such that y ▷<sub>Γₖ</sub><sup>r</sup> x'. Consequently, L<sub>Γᵢ</sub>(P<sub>Γᵢ</sub><sup>r</sup>x) > m ≥ L<sub>Γᵢ</sub>(P<sub>Γᵢ</sub><sup>r</sup>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 2<sup>m</sup>, where m is the number of labels generated at levels less than n. Clearly, the level of r-patterns in a derivation from Γ₀ is bounded by the number N<sub>[r]</sub><sup>Γ₀</sup> of distinct r-boxes occurring on Γ₀ (N<sub>[r]</sub><sup>Γ₀</sup> := |{[r]ₖt | [r]ₖt ∈ SΓ₀}|). Also, by the applicability restriction on R_T (non-subsumption), no labels can be generated at level N<sub>[r]</sub><sup>Γ₀</sup>. 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 N<sub>[r]</sub><sup>Γ₀</sup>. A label α is called r-label (in a derivation Γ₀ → Γ₁ → ...) if there are i, n, t, x such that α:[r]ₘtx ∈ Γᵢ.

**Lemma 7.4.** Let Γ₀ be an initial branch and Tr ∈ Γ₀. There is a function f : N → N such that, for every derivation Γ₀ → Γ₁ → ... and 0 ≤ n < N<sub>[r]</sub><sup>Γ₀</sup>: |{α | ∃m < n : α is an r-label generated at level m}| ≤ fn.

*Proof.* We define f by induction on n. Let Aₘ := {α | ∃k < m : α is an r-label generated at level k}. Clearly, A₀ = ∅. A new label can only be generated by an application of R_T. Therefore, by the applicability condition of R_T:

$$|A_n| \le N_{[r]}^{\Gamma_0} \cdot |\{x \mid \exists i, y : i \ge 0 \text{ and } L_{\Gamma_i}(P_{\Gamma_i}^r x) \le n - 1 \text{ and } rxy \in \Gamma_i\}|$$

By Lemma 7.3, for all n > 0:

$$|A_n| \le N_{[r]}^{\Gamma_0} \cdot \left| \bigcup_{B \subseteq A_{n-1}} \{x \mid \exists i, y : i \ge 0 \text{ and } A(P_{\Gamma_i}^r x) = B \text{ and } rxy \in \Gamma_i\} \right|$$

Then, by Lemma 7.2, there is a function g such that, for all n > 0:

$$|A_n| \le N_{[r]}^{\Gamma_0} \cdot \sum_{k=0}^{|A_{n-1}|} \binom{|A_{n-1}|}{k} \cdot gk \le N_{[r]}^{\Gamma_0} \cdot 2^{|A_{n-1}|} \cdot g(|A_{n-1}|)$$
Hence, we can define $f_0 := 0$ and, for $n > 0$, $f_n := N_{[r]}^{\Gamma_0} \cdot 2^{f(n-1)} \cdot g(f(n-1))$ □

By Lemma 7.1, for every role $r$ the number of applications of $\mathcal{R}_\diamond$ is bounded
by $\sum_{A \in \Phi} 2^{|A|} \cdot |\mathrm{Pat}^r \Gamma_0| \cdot N_{\langle r \rangle}^{\Gamma_0}$ where $\Phi := \{A \mid \exists i \ge 0: A$ is a pattern space for $r$ on $\Gamma_i\}$.
Using Lemma 7.3, this bound can be approximated from above by
$|\mathrm{Pat}^r \Gamma_0| \cdot N_{\langle r \rangle}^{\Gamma_0} \cdot N_{[r]}^{\Gamma_0} \cdot (2^{2f(N_{[r]}^{\Gamma_0})})$ where $f$ is the function from Lemma 7.4. Since
we have only finitely many roles, together with Proposition 7.2, this gives us a
bound on $|\mathcal{N}\Gamma|$ that we need for termination. Since $f$ is clearly non-elementary
in its argument, the bound is non-elementary.

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 tight.
The NEXPTIME completeness result for (nominal-free) graded modal logic over
transitive frames by Kazakov and Pratt-Hartmann [18] gives us a lower bound
for the complexity of $SOQ^+$ and hence of the decision procedure ([19] provides
no complexity bounds). Despite the potentially high worst-case complexity of
our procedure, we believe it to be well-suited for efficient implementation. In
fact, on 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 [8, 13, 12, 9, 10].

Schröder and Pattinson [24] show concept satisfiability decidable in the pres-
ence of role hierarchies and number restrictions on transitive roles, provided
the semantics is restricted to tree-like roles. They argue that the resulting logic,
PHQ, may be better suited for modeling parthood relations than the established
logics extending SH. We believe that our current approach for SOQ+ may be
adapted to obtain an efficient tableau calculus for PHQ.

**Acknowledgment.** We are grateful to our reviewers for their detailed and constructive comments.

References

1. Baader, F.: Augmenting concept languages by transitive closure of roles: An alter-native to terminological cycles. In: Mylopoulos and Reiter [20], pp. 446–451

2. De Giacomo, G., Massacci, F.: Combining deduction and model checking into tableaux and algorithms for converse-PDL. Inf. Comput. 162(1–2), 117–137 (2000)

3. Fattorosi-Barnaba, M., De Caro, F.: Graded modalities I. Stud. Log. 44(2), 197–221 (1985)
4. Fine, K.: In so many possible worlds. Notre Dame J. Form. Log. 13(4), 516–520 (1972)

5. van der Hoek, W., de Rijke, M.: Counting objects. J. Log. Comput. 5(3), 325–345 (1995)

6. Hollunder, B., Baader, F.: Qualifying number restrictions in concept languages. In: Allen, J., Fikes, R., Sandewall, E. (eds.) KR'91. pp. 335–346. Morgan Kaufmann (1991)

7. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Doherty, P., Mylopoulos, J., Welty, C.A. (eds.) KR 2006. pp. 57–67. AAAI Press (2006)

8. Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierarchies. J. Log. Comput. 9(3), 385–410 (1999)

9. Horrocks, I., Sattler, U.: Ontology reasoning in the SHOQ(D) description logic. In: Nebel, B. (ed.) IJCAI 2001. pp. 199–204. Morgan Kaufmann (2001)

10. Horrocks, I., Sattler, U.: A tableau decision procedure for SHOIQ. J. Autom. Reasoning 39(3), 249–276 (2007)

11. Horrocks, I., Sattler, U., Tobies, S.: A PSPACE-algorithm for deciding $ALCNI_{R^+}$-satisfiability. Technical Report LTCS-98-08, RWTH Aachen, Germany (1998)

12. Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for expressive description logics. In: Ganzinger, H., McAllester, D.A., Voronkov, A. (eds.) LPAR'99. LNCS, vol. 1705, pp. 161–180. Springer (1999)

13. Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for very expressive description logics. L. J. IGPL 8(3), 239–263 (2000)

14. Kaminski, M., Schneider, S., Smolka, G.: Terminating tableaux for graded hybrid logic with global modalities and role hierarchies. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 235–249. Springer (2009)

15. Kaminski, M., Smolka, G.: Hybrid tableaux for the difference modality. In: Areces, C., Demri, S. (eds.) M4M-5. ENTCS, vol. 231, pp. 241–257. Elsevier (2009)

16. Kaminski, M., Smolka, G.: Terminating tableau systems for hybrid logic with difference and converse. J. Log. Lang. Inf. 18(4), 437–464 (2009)

17. Kaminski, M., Smolka, G.: Terminating tableaux for SOQ with number restrictions on transitive roles. In: Grau, B.C., Horrocks, I., Motik, B., Sattler, U. (eds.) DL 2009. CEUR Workshop Proceedings, vol. 477 (2009)

18. Kazakov, Y., Pratt-Hartmann, I.: A note on the complexity of the satisfiability problem for graded modal logics. In: LICS 2009. pp. 407–416. IEEE Computer Society (2009)

19. 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. LNCS, vol. 4790, pp. 303–317. Springer (2007)

20. Mylopoulos, J., Reiter, R. (eds.): IJCAI'91. Morgan Kaufmann (1991)

21. Sattler, U.: Description logics for the representation of aggregated objects. In: Horn, W. (ed.) ECAI 2000. pp. 239–243. IOS Press (2000)

22. Schild, K.: A correspondence theory for terminological logics: Preliminary report. In: Mylopoulos and Reiter [20], pp. 466–471

23. Schmidt-Schauß, M., Smolka, G.: Attributive concept descriptions with complements. Artif. Intell. 48(1), 1–26 (1991)

24. Schöder, L., Pattinson, D.: How many toes do I have? Parthood and number restrictions in description logics. In: Brewka, G., Lang, J. (eds.) KR 2008. pp. 307–317. AAAI Press (2008)

25. Stirling, C., Walker, D.: Local model checking in the modal mu-calculus. Theor. Comput. Sci. 89(1), 161–177 (1991)