Tractable reasoning with vague knowledge using fuzzy $\mathcal{EL}^{++}$

Abstract

Fuzzy Description Logics (fuzzy DLs) are extensions of classic DLs that are capable of representing and reasoning with imprecise and vague knowledge. Though reasoning algorithms for very expressive fuzzy DLs have been developed and optimizations have started to be explored, the efficiency of such systems is still questionable, and the study of tractable languages is an interesting open issue. In this paper we introduce a tractable fuzzy extension of $\mathcal{EL}^{++}$. We present its syntax and semantics together with a reasoning algorithm for the fuzzy concept subsumption problem to which other problems can be reduced.

Appendix: Proofs

Proof of Lemma 1

Concept satisfiability  The claim follows easily by observing that if C is satisfiable, then there exists a model $\mathcal{I}$ of $\mathcal{C}$ and $x\in\Delta^{\mathcal{I}}$ such that $C^{\mathcal{I}}(x)>0$, therefore $C^{\mathcal{I}}(x)>\bot^{\mathcal{I}}(x)$. Thus $\mathcal{I}$ is a counter-model for $\langle C\sqsubseteq_{\mathcal{C}}\bot,1\rangle$. Similarly if $\langle C\not\sqsubseteq_{\mathcal{C}}\bot,1\rangle$, then there exists a model $\mathcal{I}$ of $\mathcal{C}$ and $x\in\Delta^{\mathcal{I}}$ such that $C^{\mathcal{I}}(x)>\bot^{\mathcal{I}}(x)=0$, the concept C is satisfiable.

Instance problem

The case follows easily by observing that $\mathcal{I}$ is a model of $\mathcal{C}\cup\mathcal{C}_{{\mathcal{A}}}$ iff it is also a model of ${\mathcal{A}}$ w.r.t. $\mathcal{C}$. More precisely, $\langle \{a\} \sqsubseteq C,d\rangle$ is just a syntactic variant of C(a) ≥ d (similarly with role assertions). More precisely, for $\mathcal{I}$ satisfying $\langle \{a\} \sqsubseteq C,d\rangle$ we have $C^{\mathcal{I}}(x)\geq\min(\{a\} ^{\mathcal{I}}(x),d)$ for every $x\in\Delta^{\mathcal{I}}$, thus also $C^{\mathcal{I}}(a)\geq\min(\{a\} ^{\mathcal{I}}(a),d)$, and by the semantics of nominals also $C^{\mathcal{I}}(a)\geq\min(1,d)=d$.

Ontology consistency

It suffices to prove that ${\mathcal{O}}$ is inconsistent iff $\langle \top\sqsubseteq_{\mathcal{C}\cup\mathcal{C}_{{\mathcal{A}}}}\bot,1\rangle$ holds:

Suppose $\langle \top\sqsubseteq_{\mathcal{C}\cup\mathcal{C}_{{\mathcal{A}}}}\bot,1\rangle$ holds. Then for every model $\mathcal{I}$ we must have that $\top^{\mathcal{I}}(x)\leq\bot^{\mathcal{I}}(x)$ for every $x\in\Delta^{\mathcal{I}}$. Obviously, $\mathcal{I}$ must be not-empty, thus there exists $c\in\Delta^{\mathcal{I}}$ such that $\top^{\mathcal{I}}(c)\leq\bot^{\mathcal{I}}(c)$. Moreover, by the definition of interpretations we have $\top^{\mathcal{I}}(c)=1$ and $\bot^{\mathcal{I}}(c)=0$, thus it follows that 1 ≤ 0, leading to absurd. Therefore ${\mathcal{O}}$ has no model.

For the opposite direction. Suppose that ${\mathcal{O}}$ is inconsistent. Since an inconsistent ontology entails all axioms we therefore have $\langle{\top}\sqsubseteq_{\mathcal{C}\cup\mathcal{C}_{{\mathcal{A}}}}\bot,{1}\rangle$.□

Example 11

In this example we want to show how the presence of, even simple, loosely fuzzy p-admissible concrete domains in fuzzy GCIs may affect the time performance of our algorithm.

Suppose that we have the concrete domain $\Theta=\langle \mathbb{Q}, \Phi^\Theta\rangle$ where ℚ corresponds to the set of rational numbers and Φ^Θ contains only the predicates $\succcurlyeq_{20}$, $\succcurlyeq_{20.5}$ as defined in Example 4. Suppose now that we also have the following ontology ${\mathcal{O}}$:

$$ {\mathcal{O}}= \{ \langle\{a\}\sqsubseteq\succcurlyeq_{20}(f),{0.5}\rangle, \langle\succcurlyeq_{20}(f)\sqsubseteq{\exists r. C},{1}\rangle, \langle{C}\sqsubseteq\succcurlyeq_{20.5}(f),{1}\rangle, \langle{C}\sqsubseteq\{a\},{1}\rangle \} $$

and the admissibility restriction on Rule CR8a does not apply. At some point of the execution of the algorithm we will have the following application of rules:

$$ \begin{tabular}{ ll } \par \vdots \tabularnewline \textbf{ CR3} & { $\dfrac{ \langle \{a\}\sqsubseteq \succcurlyeq_{20}(f),0.5\rangle }{ \langle \{a\}\sqsubseteq\exists r.C,0.5\rangle }: $ } $\langle \succcurlyeq_{20}(f)\sqsubseteq\exists r.C,1\rangle $ \tabularnewline\tabularnewline \textbf{ CR6} & { $\dfrac{ \langle \{a\}\sqsubseteq\{ a\} ,1\rangle , \langle C\sqsubseteq\{ a\} ,1\rangle , \langle \{ a\} \rightsquigarrow C,0.5\rangle , \langle C\sqsubseteq \succcurlyeq_{20.5}(f),1\rangle } { \langle \{a\}\sqsubseteq \succcurlyeq_{20.5}(f),0.5\rangle } $ } \tabularnewline\tabularnewline \par \textbf{ CR8} & { $\dfrac{ \langle\{a\}\sqsubseteq\succcurlyeq_{20.5}(f),{0.5}\rangle }{ \langle\{a\}\sqsubseteq\succcurlyeq_{20}(f),{0.6}\rangle }: $ } $\succcurlyeq_{20.5}(f)\geq 0.5 \models \succcurlyeq_{20}(f)\geq 0.6$ \par \tabularnewline\tabularnewline \textbf{ CR3} & { $\dfrac{ \langle \{a\}\sqsubseteq \succcurlyeq_{20}(f),0.6\rangle }{ \langle \{a\}\sqsubseteq\exists r.C,0.6\rangle }: $ } $\langle \succcurlyeq_{20}(f)\sqsubseteq\exists r.C,1\rangle $ \tabularnewline \vdots \end{tabular} $$

The implication $\succcurlyeq_{20.5}(f)\geq 0.5 \models \succcurlyeq_{20}(f)\geq 0.6$ can be derived from the $\succcurlyeq_{20.5},\succcurlyeq_{20}$ membership functions presented in Fig. 3. As it can be seen, these rules will be repeatedly applied until the algorithm reaches $\langle \{a\}\sqsubseteq\exists r.C,1\rangle$ while the number of repetitions of the rule application depends on the form of the $\succcurlyeq_{20.5},\succcurlyeq_{20}$ membership functions.

Fig. 3

The $\succcurlyeq_{20}$ and $\succcurlyeq_{20.5}$ membership functions

Therefore without the strict p-admissibility restrictions our algorithm becomes non-polynomial.

Proposition 1

The concrete domain presented in Example 4, without the presence of $\succcurlyeq$ _{+  q} predicates, is loosely fuzzy p -admissible.

Sketch Proof

The corresponding concrete domain contains an unary predicate $\succcurlyeq_{q}$ for every q ∈ ℚ defined on the f _q function presented in Example 4. The f _q function maps elements of ℚ to the [0,1] interval. We build another function g _q :[0,1]→ℚ as follows:

$$ g_{q}(x)= \begin{cases} -\infty \quad,\ x=0\\ x\cdot10-10+q \quad, \ x\in(0,1] \end{cases} $$

and it can be verified that f _q (g _q (x)) = x for every x ∈ (0,1]. Suppose now that we have the following conjunction of formulae with degrees:

$$ \bigwedge\limits_{i=1}^k \succcurlyeq_{q_i}(x_i)\geq d_i $$

Each conjunct of the form $\succcurlyeq_{q_i}(x_i)\geq d_i$ can be transformed to some inequality x _i  ≥ g _q (d _i ). Therefore we end up with a system of inequalities which can be reduced to the concrete domain of rational numbers presented in Baader et al. (2005). The latest has been proved to be a convex concrete domain for which satisfiability and implication are decidable in polynomial time.

We now examine why the corresponding concrete domain will lose its convexity when it allows for conjuncts of the form $\succcurlyeq$ ₊ $_{q_i}(x_i,y_i)\geq d_i$. These conjuncts can also be transformed to inequalities x ≥ g _q (d _i ) + y and therefore the initial problem is reduced to solving a system of inequalities. Unfortunately it is easy to show by a counter example that the corresponding concrete domain is non-convex. For example x ≥ 10 and y ≥ 10 imply that either x ≥ y + 0 or y ≥ x + 0 holds, but none of the previous two disjuncts will always apply. □

Proof of Lemma 2

The linear time complexity of the normalization process is an immediate consequence of the fact that the normalization algorithm is identical to the one presented for the crisp ${\mathcal{EL}^{++}}$ language (Baader et al. 2005).

For the other part it suffices to prove that each model of ${\mathcal{O}}^{\prime}$ is also a model of ${\mathcal{O}}$ and each model of ${\mathcal{O}}$ can be extended to a model of ${\mathcal{O}}^{\prime}$ by appropriately interpreting new concept and role names. The proof is by induction on each of the substitutions performed by the rules. We will only present the case of rule NF2.

Let $\mathcal{I}^{\prime}$ be a model of ${\mathcal{O}}^{\prime}$. Then, for every $x\in\Delta^{\mathcal{I}^{\prime}}$, we have $\hat{D}^{\mathcal{I}^{\prime}}(x)\leq A^{\mathcal{I}^{\prime}}(x)$ and $\min(C^{\mathcal{I}^{\prime}}(x),A^{\mathcal{I}^{\prime}}(x),d)\leq E^{\mathcal{I}^{\prime}}(x)$, thus $\min(C^{\mathcal{I}^{\prime}}(x),\hat{D}^{\mathcal{I}^{\prime}}(x),d)\leq E^{\mathcal{I}^{\prime}}(x)$ and therefore $\mathcal{I}^{\prime}$ is also a model of ${\mathcal{O}}$.

Let now $\mathcal{I}$ be a model of ${\mathcal{O}}$. We create an interpretation $\mathcal{I}^{\prime}$ that is identical to $\mathcal{I}$ with the difference that $A^{\mathcal{I}^{\prime}}(x)=\hat{D}^{\mathcal{I}}(x)$ for every $x\in\Delta^{\mathcal{I}}$. Since A is new, it only appears in the concept inclusions $\langle{\hat{D}}\sqsubseteq A,1\rangle$ and $\langle C\sqcap A\sqsubseteq E,d\rangle$. It can be easily verified that both concept inclusions are satisfied by $\mathcal{I}^{\prime}$. Therefore $\mathcal{I}^{\prime}$ is a model of ${\mathcal{O}}^{\prime}$.□

Proposition 2

For every strictly fuzzy p -admissible concrete domain ${\mathcal{D}}$ and arbitrary number $\mbox{\ensuremath{d_{\omega}\in(0,1)}}$ the following holds: If δ is a solution for the conjunction ${\textnormal{conj}}$ , then there also exists a solution δ′′ such that (i) $p^{{\mathcal{D}}}(\delta^{\prime\prime}(\overline{X}))=1$ if $p^{\mathcal{D}}(\delta(\overline{X}))>d_{\omega}$ and (ii)  $p^{\mathcal{D}}(\delta^{\prime\prime}(\overline{X}))=p^{\mathcal{D}}(\delta(\overline{X}))$ if $p^{\mathcal{D}}(\delta(\overline{X}))\leq d_{\omega}$ for every predicate $p\in\Phi^{\mathcal{D}}$.

Proof

Based on the mapping δ we build two new conjunctions as follows:

$$\begin{array}{rll} {\textnormal{conj}}^{\prime}&:= & \underset{\textnormal{if } p^{\mathcal{D}}\left(\delta\left(\overline{X}\right)\right)=d} {\bigwedge}p\big(\overline{X}\big)\geq d \\ {\textnormal{conj}}^{\prime\prime}&:= & \underset{\textnormal{if }p^{\mathcal{D}}\left(\delta\left(\overline{X}\right)\right)=d\textnormal{ and }d\leq d_{\omega}} {\bigwedge}p\big(\overline{X}\big)\geq d {\bigwedge} \underset{\textnormal{if }p^{\mathcal{D}}\left(\delta\left(\overline{X}\right)\right)=d\textnormal{ and }d>d_{\omega}} {\bigwedge} p\big(\overline{X}\big)\geq 1. \end{array}$$

Obviously every solution of conj′′ is also a solution of conj. Therefore if δ′′ is a solution for conj′′ it is also a solution for conj.

We first prove that conj″ has at least one solution. Based on Property 2 of Definition 2 we can easily show that if there exists no solution for ${\textnormal{conj}}^{\prime\prime}$, then there exists no solution for ${\textnormal{conj}}$ which is absurd since we have already assumed that δ is a solution for ${\textnormal{conj}}$.

It remains to prove that there exists a solution of the form δ′′ for ${\textnormal{conj}}^{\prime\prime}$. We assume the opposite: Suppose that S′′ is the (possibly infinite) set of solutions of ${\textnormal{conj}}^{\prime\prime}$ then there exists no solution δ _j ′′ ∈ S′′ that corresponds to δ′′. This implies that for every solution δ _j ′′ there exists some predicate p _j and a vector of variables $\overline{X}_j$ such that (i) $p_j^{\mathcal{D}}(\delta_j^{\prime\prime}(\overline{X}_j))= d_j$ and (ii) $p_j(\overline{X_j})\geq d_j$ does not appear as a conjunct in ${\textnormal{conj}}^{\prime\prime}$. We create a set S′′ _p as follows: for every solution δ _j ′′ in S′′ the set S′′ _p contains an inequality $p_j(\overline{X}_j)\geq d_j$ such that conditions (i) and (ii) apply. The latest implies that

$$ {\textnormal{conj}}^{\prime\prime}\models \bigvee\limits_{p_j(\overline{X}_j)\geq d_j\in S_p^{\prime\prime}}p_j(\overline{X}_j)\geq d_j $$

and Property 2 of Definition 1 (convexity) ensures that

$$ {\textnormal{conj}}^{\prime\prime}\models p_\lambda(\overline{X}_\lambda)\geq d_\lambda $$

for some element $p_\lambda(\overline{X}_\lambda)\geq d_\lambda$ appearing in S _p ′′.

Case d_λ > d_ω 1

We consider the number $d_\omega^+$ that is slightly larger than d _ω and we create the conjunctions:

• 1. ${\textnormal{conj}}^{\prime}_{d_\omega^+}$ by replacing every degree d in ${\textnormal{conj}}^{\prime}$ with min (d,d _ω ),

• 2. ${\textnormal{conj}}^{\prime\prime}_{d_\omega^+}$ by replacing every degree d in ${\textnormal{conj}}^{\prime\prime}$ with min (d,d _ω ).

It can be verified that the two conjunctions are identical. Since ${\textnormal{conj}}^{\prime\prime}\models p_\lambda(\overline{X}_\lambda)\geq d_\lambda$, Property 1 of Definition 2 ensures that ${\textnormal{conj}}^{\prime\prime}_{d_\omega^+}\models p_\lambda(\overline{X}_\lambda)\geq \min(d_\lambda,d_\omega^+)=d_\omega^+$. Since ${\textnormal{conj}}^{\prime}_{d_\omega^+}$ and ${\textnormal{conj}}^{\prime\prime}_{d_\omega^+}$ are identical we also have that ${\textnormal{conj}}^{\prime}_{d_\omega^+}\models p_\lambda(\overline{X}_\lambda)\geq d_\omega^+$. The latest implies that $p_\lambda^{\mathcal{D}}(\delta(\overline{X}_\lambda))>d_\omega$ and by construction of ${\textnormal{conj}}^{\prime\prime}$ we have that $p_\lambda(\overline{X}_\lambda)\geq 1$ appears in ${\textnormal{conj}}^{\prime\prime}$ which contradicts the assumption that no solution δ _λ corresponds to δ′′.

Case  d_λ > d_ω 2

In a similar way than before, we show that $p_\lambda(\overline{X}_\lambda)\geq d_\lambda$ will appear in ${\textnormal{conj}}^{\prime\prime}$, which also contradicts our assumption.

Therefore we have that there exists a solution δ′′.□

Proof of Lemma 3

Let $\langle C\sqsubseteq_{{\mathcal{O}}}D,d\rangle$, we need to show that $\langle \{ o\} \sqsubseteq_{{\mathcal{O}}^{\prime}}B,d\rangle$ holds. Since ${\mathcal{O}}^{\prime}$ extends ${\mathcal{O}}$, every model $\mathcal{I}^{\prime}$ of ${\mathcal{O}}^{\prime}$ is also a model of ${\mathcal{O}}$. Therefore $\langle C\sqsubseteq_{{\mathcal{O}}^{\prime}}D,d\rangle$ and since ${\mathcal{O}}^{\prime}$ contains $\langle{\{o\}}\sqsubseteq{C},{1}\rangle$, $\langle{D}\sqsubseteq{B},{1}\rangle$, it can be easily verified that $\langle \{ o\} \sqsubseteq_{{\mathcal{O}}^{\prime}}B,d\rangle$ holds.

For the opposite direction we will show the contrapositive, i.e. that $\langle C \not \sqsubseteq_{{\mathcal{O}}} D,d\rangle$ implies $\langle \{o\} \not \sqsubseteq_{{\mathcal{O}}} B,d\rangle$.

If $\langle C \not \sqsubseteq_{{\mathcal{O}}} D,d\rangle$ then there exists an interpretation $\mathcal{I}$ s.t. $C^{\mathcal{I}}(\omega)>D^{\mathcal{I}}(\omega)$, $d>D^{\mathcal{I}}(\omega)$ for some $\omega\in\Delta^\mathcal{I}$. We build an interpretation $\mathcal{I}^{\prime}$ that is identical to $\mathcal{I}$ with the following differences: (i) $A^{\mathcal{I}^{\prime}}(x)=1$ if $A^{\mathcal{I}}(x)>D^\mathcal{I}(\omega)$ for every $x\in\Delta^\mathcal{I}$ and concept name A, (ii) $p^{\mathcal{I}^{\prime}}(\overline F)(x)=1$ if $p^{\mathcal{I}}(\overline F)(x)>D^\mathcal{I}(\omega)$ for every $x\in\Delta^\mathcal{I}$ and concept $p(\overline F)$ where p is a predicate belonging to some loose fuzzy p-admissible concrete domain (Proposition 2 ensures that such an interpretation can be constructed). (iii) $r^{\mathcal{I}^{\prime}}(x,y)=1$ if $r^{\mathcal{I}}(x,y)>D^\mathcal{I}(\omega)$ for every $x,y\in\Delta^\mathcal{I}$ and $r\in R_{\mathcal{O}}$, (iv) $o^\mathcal{I}=\omega$ and $B^\mathcal{I}(x)=D^\mathcal{I}(x)$ for every $x\in\Delta^\mathcal{I}$.

If the interpretation $\mathcal{I}$ satisfies a concept inclusion of the form $\langle{\Gamma_1}\sqsubseteq{\Gamma_2},{d}\rangle$, where Γ₁, Γ₂ are concept descriptions, it can be verified that $\mathcal{I}^{\prime}$ also satisfies the particular concept inclusion (the same applies for role inclusions). Therefore $\mathcal{I}^{\prime}$ is a model of ${\mathcal{O}}$ and since by construction of $\mathcal{I}^{\prime}$ it also satisfies the concept inclusions $\langle{\{o\}}\sqsubseteq{C},{1}\rangle$, $\langle{D}\sqsubseteq{B},{1}\rangle$ , it is also a model of ${\mathcal{O}}^{\prime}$. The latest finishes our proof since $\min(\{o\}^{\mathcal{I}^{\prime}}(\omega),d)=\min(\{o\}^{\mathcal{I}^{\prime}}(o^{\mathcal{I}^{\prime}}),d)=d$, $D^{\mathcal{I}^{\prime}}(\omega)=D^{\mathcal{I}}(\omega)$, and $d>D^\mathcal{I}(\omega)$.□

Proof of Lemma 4

In the following |·| denotes the cardinality of a set. We also use the standard notion of big-O from computational complexity, denoted by O. The polynomial complexity of the algorithm is a result of the following properties.

• At each step of the algorithm the maximum number of concept inclusions in the saturated ontology is bounded by $|BC_{{\mathcal{O}}}|^{2}$. This is due to the fact that for two inclusions $\langle C\sqsubseteq D,d\rangle$ and $\langle C\sqsubseteq D,d^{\prime}\rangle$ only the one with the higher degree is kept. On the other hand the number of concept inclusions of the form $\langle C\sqsubseteq\exists r.D,d\rangle$ is bounded by $|R_{{\mathcal{O}}}|\cdot|BC_{{\mathcal{O}}}|^{2}$. Since each concept and role inclusion, in its normal form, contains at most 3 concept and roles we can conclude that $|BC_{{\mathcal{O}}}|$ and $|R_{{\mathcal{O}}}|$ have sizes $O(|{\mathcal{O}}|)$. Therefore there are at most $O(|{\mathcal{O}}|^{3})$ concept inclusions in the saturated ontology.

• Rule CR8b, that may introduce degrees that are not in $[0,1]_{{\mathcal{O}}}$, can only be applied once for each pair of nominal—ordinary predicate concept description. Since there exist $O(|{\mathcal{O}}|^2)$ such pairs in our ontology, at most $O(|{\mathcal{O}}|^2)$ new degrees can be introduced.

• None of the other rules introduces new degrees (rule CR8a does not introduce any new degrees due to Property 3 of Definition 2). Therefore the degree d in some concept inclusion $\langle C\sqsubseteq D,d\rangle$ or $\langle C\sqsubseteq\exists r.D,d\rangle$ can be altered at most $O(|{\mathcal{O}}|^2)$ times.

• From the above points we can conclude that there can be at most $O(|{\mathcal{O}}|^{5})$ applications of rules CR1–CR13.

• It takes polynomial time in the size of $|{\mathcal{O}}|$ to check if some rule is applicable. For all rules except rules CR6, CR7, CR8 for a naive application of the algorithm it is evident that the checks that should be made (checking for each concept inclusion in ${\mathcal{O}}$ all fuzzy concept inclusions in ${{\mathcal{O}}_{\rm SAT}}$) cannot be more then $O(|{\mathcal{O}}|\cdot|{{\mathcal{O}}_{\rm SAT}}|)=|{\mathcal{O}}|^{4}$.

• Rules CR7, CR8 can be applied in polynomial time due to Property 1 of Definition 1.

• For rule CR6 the problem of finding if $\langle \{a\} \rightsquigarrow D,d\rangle$ can be solved by using a variation of the shortest path problem (for weighted directed graphs). In Fig. 4 we see such a graph where each node corresponds to some element of $BC_{{\mathcal{O}}}$ and each edge from node C _i to C _j has length

  $$ |d_{C_{i},C_{j}}|=\inf \left\{ \frac{1}{d}\mid r\in R_{{\mathcal{O}}}\textnormal{ and }\langle{C_{i}}\sqsubseteq{\exists r.C_{j}},d\rangle\in{{\mathcal{O}}_{\rm SAT}}\right\} . $$

  As it can be seen in Fig. 4 edges with ∞ length are not taken into account. In our variation of the shortest path problem we consider that the distance traveled along two edges with lengths e ₁,e ₂ is max (e ₁,e ₂) instead of e ₁ + e ₂. Obviously if the shortest path from some $\{a\} \in BC_{{\mathcal{O}}}$ to D has length e we can conclude that $\langle C\rightsquigarrow D,\frac{1}{d}\rangle$. The problem of finding all the shortest paths in a graph, by using a variation of the “FloydWarshall algorithm”, has $O(|{\mathcal{O}}|^{3})$ complexity (Floyd 1962). Therefore applicability check for rule CR6 also takes polynomial time.□

Fig. 4

Reducing $\langle \{a\} \rightsquigarrow C\rangle ,d$ to the shortest path problemFigure 4–was extracted from MS PDF. Please check if correct.

Proof of Theorem 1

(Soundness) Soundness is the if direction of Theorem 1. Assume that the algorithm is applied to an ontology ${\mathcal{O}}$ creating a saturated one ${{\mathcal{O}}_{\rm SAT}}$, and let { o} and B be a nominal and a concept name such that either Condition S1 or S2 holds. To show that $\langle \{ o\} \sqsubseteq_{{\mathcal{O}}}B,d\rangle$ holds, we first prove the following claim:

Claim

Each concept inclusion in ${{\mathcal{O}}_{\rm SAT}}$ is satisfied by a model $\mathcal{I}$ of ${\mathcal{O}}$.

Proof

We show the claim using induction over the application of the completion rules in Table 7.

For the base case, initially no rule is applied and ${{\mathcal{O}}_{\rm SAT}}$ is empty, so any model of ${\mathcal{O}}$ is also a model of ${{\mathcal{O}}_{\rm SAT}}$ and the claim follows trivially.

For the induction step, we assume that at step j we have computed ${{\mathcal{O}}_{\rm SAT}^{j}}$ and all subsumptions in it are satisfied. Then at step j + 1 some rule from Table 7 is applied and a new subsumption is added to create ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. We make a case distinction according to the rule that was applied to generate and add the new subsumption. For the rest of the proof we consider that $C^{\mathcal{I}}(x)=e$.

(I1 or I2):

These rules add $\langle C \sqsubseteq C ,1\rangle$ and $\langle C\sqsubseteq\top,1\rangle$ to ${{\mathcal{O}}_{\rm SAT}}$ for every concept $C\in BC_\mathcal{C}$. By the semantics of every $C\in BC_\mathcal{C}$ and the top concept the claim follows trivialy.

(CR1):

This implies that there is $\langle C\sqsubseteq E,d_{1}\rangle \in{{\mathcal{O}}_{\rm SAT}^{j}}$, and $\langle E\sqsubseteq D,d_{2}\rangle \in{\mathcal{O}}$ and the rule adds $\langle C\sqsubseteq D,{\min(d_{1},d_{2})}\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. It remains to show that $D^{\mathcal{I}}(x)\geq \min(e,d_{1},d_{2})$. By IH we have that $E^{\mathcal{I}}(x)\geq \min(e,d_{1})$ which together with $\langle E\sqsubseteq D,d_{2}\rangle$ imply that

$$ D^{\mathcal{I}}(x)\geq \min \big(E^{\mathcal{I}}(x),d_{2}\big)\geq \min(e,d_{1},d_{2}). $$

(CR2):

This implies that there are subsumptions of the form $\langle C\sqsubseteq C_{1},d_{1}\rangle,$ $\langle C\sqsubseteq C_{2},d_{2}\rangle \in{{\mathcal{O}}_{\rm SAT}^{j}}$, and $\langle C_{1}\sqcap C_{2}\sqsubseteq D,d_{3}\rangle \in{\mathcal{O}}$ and the rule adds $\langle C\sqsubseteq D, \min(d_{1},d_{2},d_{3})\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. It remains to show that $D^{\mathcal{I}}(x)\geq \min(e,d_{1},d_{2},d_{3})$. By IH we have $C_{1}^{\mathcal{I}}(x)\geq \min(e,d_{1})$ and $C_{2}^{\mathcal{I}}(x)\geq \min(e,d_{2})$ which together with $\langle C_{1}\sqcap C_{2}\sqsubseteq D,d_{3}\rangle$ give

$$ D^{\mathcal{I}}(x)\geq \min \big(C_{1}^{\mathcal{I}}(x),C_{2}^{\mathcal{I}}(x),d_{3}\big)\geq \min(e,d_{1},d_{2},d_{3}). $$

(CR3):

This implies that there exists a subsumption of the form $\langle C\sqsubseteq C^{\prime},d_{1}\rangle \in{{\mathcal{O}}_{\rm SAT}^{j}}$, and $\langle C^{\prime}\sqsubseteq\exists r.D,d_{2}\rangle \in{\mathcal{O}}$ and the rule adds $\langle{C^{\prime}} \sqsubseteq{\exists r.D}, {\min(d_1,d_2}\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. It remains to show that $(\exists r.D)^\mathcal{I}(x)\geq \min(e,d_1,d_2)$. By IH we have $E^\mathcal{I}(x)\geq\min(e,d_1)$ which together with $\langle C^{\prime}\sqsubseteq\exists r.D,d_{2}\rangle$ imply that

$$ (\exists r.D)^\mathcal{I}(x)\geq\min(e,d_1,d_2). $$

(CR4):

This implies that there are subsumptions of the form $\langle C\sqsubseteq\exists r.E,d_{1}\rangle$, $\langle E\sqsubseteq C^{\prime},d_{2}\rangle\in{{\mathcal{O}}_{\rm SAT}^{j}}$, and $\langle \exists r.C^{\prime}\sqsubseteq D,d_{3}\rangle\in{\mathcal{O}}$ and the rule adds $\langle C\sqsubseteq D, \min(d_{1},d_{2},d_{3})\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. It remains to show that $D^\mathcal{I}(x)\geq \min(e,d_1,d_2,d_3)$. By IH we have that $(\exists r.E)^\mathcal{I}(x) \geq \min(e,d_1)$ and that ${C^{\prime}}^\mathcal{I}(y)\geq \min(E^\mathcal{I}(y),d_2)$ for all $y\in\Delta^\mathcal{I}$ which together with the semantics of existential restrictions imply that $(\exists r.C^{\prime})^\mathcal{I}(x) \geq \min(e,d_1,d_2)$. The latest inequality along with $\langle \exists r.C^{\prime}\sqsubseteq D,d_{3}\rangle$ give

$$ D^\mathcal{I}(x)\geq\min(e,d_1,d_2,d_3). $$

(CR5):

This implies that there are subsumptions of the form $\langle C\sqsubseteq\exists r.E,d_{1}\rangle$, $\langle E\sqsubseteq\bot,d_{2}\rangle \in{{\mathcal{O}}_{\rm SAT}^{j}}$ and the rule adds $\langle C\sqsubseteq\bot,1\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. It remains to show that e = 0. By IH we have $(\exists r.E)^\mathcal{I}(x)\geq \min(e,d_1)$ and $\bot^\mathcal{I}(y)\geq \min(E^\mathcal{I}(y),d_2)$ for all $y\in\Delta^\mathcal{I}$. The latest inequality implies that $E^\mathcal{I}(y)=0$ for all $y\in\Delta^\mathcal{I}$ which together with the semantics of existential restrictions give that $(\exists r.E)^\mathcal{I}(x)=0$. Therefore, and since $(\exists r.E)^\mathcal{I}(x)\geq \min(e,d_1)$ and d ₁ > 0, we have that

$$e=0.$$

(CR6):

This implies that there are subsumptions of the form $\langle{C}\sqsubseteq{\{a\}},{1}\rangle$, $\langle{E}\sqsubseteq{\{a\}},{1}\rangle$ ,$\langle{E}\sqsubseteq{D},{d_2}\rangle$ in ${{\mathcal{O}}_{\rm SAT}^{j}}$, and $\langle \{b\}\rightsquigarrow E,d_1\rangle$ and the rule adds $\langle{C}\sqsubseteq{D},{\min(d_1,d_2)}\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. It remains to show that $D^\mathcal{I}(x)\geq \min(e,d_1,d_2)$. By IH we have that

$$ \{a\}^\mathcal{I}(x) \geq e $$

(4)

$$ \{a\}^\mathcal{I}(y) \geq E^\mathcal{I}(y) $$

(5)

$$ D^\mathcal{I}(y) \geq \min\big(E^\mathcal{I}(y),d_2\big) $$

(6)

for every $y\in\Delta^\mathcal{I}$. The $\langle \{b\}\rightsquigarrow E,d_1\rangle$ condition along with the IH imply that

$$ (\exists r_1. (...\exists r_k.E))^\mathcal{I}(y)\geq \min\big(\{b\}^\mathcal{I}(y),d_1\big) $$

(7)

for some arbritrary sequence of roles r ₁,...,r _k .

• (i) If $x\neq a^\mathcal{I}$ we have that $\{a\}^\mathcal{I}(x)=0$ which together with (4) imply that e = 0 and therefore $D^\mathcal{I}(x)\geq \min(e,d_1,d_2)$ trivially applies.

• (ii) If $x=a^\mathcal{I}$, then by substituting in (7) y with $b^\mathcal{I}$ we get that $(\exists r_1. (...\exists r_k.E))^\mathcal{I}(b^\mathcal{I})\geq d_1$. The latest inequality together with the semantics of existential restrictions imply that there exists some $z\in\Delta^\mathcal{I}$ such that $E^\mathcal{I}(z)\geq d_1$. The fact that $E^\mathcal{I}(z)\geq d_1$ along with (5) imply that $E^\mathcal{I}(a^\mathcal{I})\geq d_1$ which combined with (6) implies that

  $$ D^\mathcal{I}(a^\mathcal{I})\geq\min(d_1,d_2)\geq\min(e,d_1,d_2). $$

(CR7):

This implies that there are subsumptions of the form $\langle C\sqsubseteq{p_{i}(\overline{F}_{i})},{d_{i}}\rangle\in{{\mathcal{O}}_{\rm SAT}^{j}}$ for 1 ≤ i ≤ m, and $\bigwedge_{i=1}^{m}p_{i}(\overline{F}_{i})\geq d_{i}$ is unsatisfiable and the rule adds $\langle{C}\sqsubseteq{\bot}, {1}\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. It remains to show that e = 0. We proceed by contradiction. Let e > 0, by IH we have that $p^\mathcal{I}_i(\overline{F}_i)\geq\min(e,d)$ for all 1 ≤ i ≤ m. A mapping $\delta:N_F\rightarrow \Delta^{\mathcal{D}}$ is built as follows: $\delta(\overline{F}_i)=\overline{F}^\mathcal{I}_i(x)$ for all 1 ≤ i ≤ m. It can be verified that δ is a solution for $\bigwedge_{i=1}^{m}p_{i}(\overline{F}_i)\geq\min(e,d_{i}).$ But, according to Property 2 of Definition 2 and since $\bigwedge_{i=1}^{m}p_{i}(\overline{F}_{i})\geq d_{i}$ is unsatisfiable the previous conjunction should also be unsatisfiable. Therefore the assumption we have made is wrong, implying that

$$e=0.$$

(CR8a):

This implies that there are subsumptions of the form $\langle{C}\sqsubseteq{p_i(\overline{F}_i)},{d_i}\rangle\in{{\mathcal{O}}_{\rm SAT}^{j}}$ for 1 ≤ i ≤ m, and $\bigwedge_{i=1}^{m}p_{i}(\overline{F}_{i})\geq d_{i}\models p(\overline{F})\geq d$ and the rule adds $\langle{C}\sqsubseteq{p(\overline{F})},{d}\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. It remains to show that $p^{\mathcal{I}}(\overline{F})\geq\min(e,d)$. A mapping δ is built as before: $\delta(\overline{F}_i)=\overline{F}^\mathcal{I}_i(x)$ for all 1 ≤ i ≤ m. It can be verified that $\delta\models\bigwedge_{i=1}^{m}p_{i}(\overline{F}_i)\geq\min(e,d_{i})$ and Property 1 of Definition 2 ensures that

$$ \bigwedge\limits_{i=1}^{m}p_{i}(\overline{F}_{i})\geq\min(e,d_{i})\models p(\overline{F})\geq\min(e,d). $$

Since δ is a solution for the conjunction we have that $\delta\models p(\overline{F})\geq\min(e,d)$, and by construction of δ that

$$ p^{\mathcal{I}}(\overline{F})(x)\geq\min(e,d). $$

(CR8b):

The proof for loose fuzzy p-admissible concrete domains can be performed as before, keeping in mind that C will always correspond to a nominal {a} due to the restriction presented in (3) and therefore either $C^{\mathcal{I}}(x)=0$ or $C^{\mathcal{I}}(x)=1$ will hold.

(CR9):

This implies that there are subsumptions of the form $\langle C\sqsubseteq{p_{k}(\overline{F}_{k})},{d_{k}}\rangle$, $\langle C\sqsubseteq{p_{l}(\overline{F}_{l})}, {d_{l}}\rangle\in{{\mathcal{O}}_{\rm SAT}^{j}}$ such that $p_{k}\in\Phi^{\mathcal{D}_{k}}$, $p_{l}\in\Phi^{\mathcal{D}_{l}}$ with ${\mathcal{D}}_{k}\not={\mathcal{D}}_{l}$, and the feature vectors $\overline{F}_{k},\ \overline{F}_{l}$ have a common feature f and the rule adds $\langle{C}\sqsubseteq{\bot},{1}\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. It remains to show that e = 0. By IH we have that $p^\mathcal{I}_k(\overline{F}_k)\geq \min(e,d_k)$ and $p^\mathcal{I}_l(\overline{F}_l)\geq \min(e,d_l)$. If e > 0, and since d _k  > 0 and d _l  > 0, it is implied by the semantics of fuzzy concrete domains that $f^{\mathcal{I}}(x)=y$ for some $y\in\Delta^{\mathcal{D}_{i}}\bigcap\Delta^{\mathcal{D}_{j}}$, contradicting the disjointness of $\Delta^{\mathcal{D}_{i}}$ and $\Delta^{\mathcal{D}_{j}}$. Thus

$$e=0.$$

(CR10):

This implies that there exists a subsumption of the form $\langle C\sqsubseteq\exists r.D,d\rangle \in{{\mathcal{O}}_{\rm SAT}^{j}}$, and $r\sqsubseteq s\in{\mathcal{O}}$ and the rule adds $\langle C\sqsubseteq\exists s.D,d\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. It remains to show that $(\exists s.D)^\mathcal{I}(x)\geq \min(e,d)$. By IH we have $(\exists r.D)^\mathcal{I}(x)\geq \min(e,d)$ which together with $r\sqsubseteq s$ imply that

$$(\exists s.D)^\mathcal{I}(x)\geq \min(e,d).$$

(CR11):

This implies that there are subsumptions of the form $\langle{C}\sqsubseteq{\exists r_1.E},{d_1}\rangle$, $\langle{E}\sqsubseteq{\exists r_2.D},{d_2}\rangle\in{{\mathcal{O}}_{\rm SAT}^{j}}$, and $r_1\circ r_2\sqsubseteq s\in{\mathcal{O}}$, and the rule adds $\langle{C}\sqsubseteq{\exists s.E},{\min(d_1,d_2)}\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. It remains to show that $(\exists s.E)^\mathcal{I}(x)\geq \min(e,d_1,d_2)$. By IH and the semantics of existential restrictions we have that

$$\begin{array}{rll} \sup\limits_{y\in\Delta^{\mathcal{I}}}\big\{\min(r_{1}^{\mathcal{I}}(x,y),E^{\mathcal{I}}(y))\big\}& \geq & \min(e,d_{1}) \\ \sup\limits_{z\in\Delta^{\mathcal{I}}}\big\{\min(r_{2}^{\mathcal{I}}(y,z),D^{\mathcal{I}}(z))\big\}& \geq& \min \big(E^{\mathcal{I}}(y),d_{2}\big). \end{array}$$

By combining these two inequalities we get that

$$ \sup\limits_{y,z\in\Delta^{\mathcal{I}}} \big\{\min(r_{1}^{\mathcal{I}}(x,y),r_{2}^{\mathcal{I}} (y ,z),D^{\mathcal{I}}(z))\big\} \geq \min(e,d_{1},d_{2}) $$

or equivalently

$$ \sup\limits_{z\in\Delta^{\mathcal{I}}} \big\{\min ( (r_1\circ r_2)^\mathcal{I}(x,z), D^{\mathcal{I}}(z) ) \big\} \geq \min(e,d_{1},d_{2}) $$

which together with $r_1\circ r_2 \sqsubseteq s$ implies that

$$ (\exists s.E)^\mathcal{I}(x)\geq \min(e,d_1,d_2). $$

(CR12):

This implies that there exists a subsumption of the form $\langle{C}\sqsubseteq{\{a\}},{d}\rangle\in{{\mathcal{O}}_{\rm SAT}^{j}}$ with d > 0 and $\langle{C}\sqsubseteq{\{a\}},{1}\rangle$ is added to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. It remains to show that $\{a\}^\mathcal{I}(x)\geq e$. By IH we have that $\{a\}^\mathcal{I}(x)\geq \min(e,d)$ and since the value of $\{a\}^\mathcal{I}(x)$ is either 0 or 1, d > 0, and e ∈ [0,1], it is implied that

$$ \{a\}^\mathcal{I}(x)\geq e. $$

□

If Condition S1 holds, i.e. $\langle{\{o\}}\sqsubseteq{D},{d^{\prime}}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ for some d′ ≥ d, then by the previous Claim $D^\mathcal{I}(x)\geq \min(\{o\}^\mathcal{I}(x),d^{\prime})\geq \min(\{o\}^\mathcal{I}(x),d)$ for every model $\mathcal{I}$ of ${\mathcal{O}}$. The latest inequality implies that $\langle\{o\}\sqsubseteq_{\mathcal{O}} {B},{d}\rangle$. If Condition S2 holds, i.e. $\langle{\{a\}}\sqsubseteq{\bot},{1}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ for some arbritrary nominal $\{a\}\in BC_{\mathcal{O}}$, then by the previous claim $\{a\}^\mathcal{I}(a^\mathcal{I})\leq\bot^\mathcal{I}(a^\mathcal{I})=0$ which entails that ${\mathcal{O}}$ is inconsistent. Since an inconsistent ontology entails all axioms we therefore have $\langle\{o\}\sqsubseteq_{\mathcal{O}} {B},{d}\rangle$.□

Proposition 3

If $\langle{\top}\sqsubseteq{F},{d}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ for some concept description F then for every $C\in BC_\mathcal{C}$ it holds that $\langle{C}\sqsubseteq{F},{d^{\prime}}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ for some degree d′ ≥ d.

Proof

Suppose that our algorithm is performed on m steps and the saturated ontology on step j is denoted with ${{\mathcal{O}}_{\rm SAT}^{j}}$ (we will use ${{\mathcal{O}}_{\rm SAT}}$ as a shortcut for ${{\mathcal{O}}_{\rm SAT}^{m}}$). We prove this by induction on the smallest j such that $\langle{\top}\sqsubseteq{D},{d}\rangle\in {{\mathcal{O}}_{\rm SAT}^{j+1}}\setminus{{\mathcal{O}}_{\rm SAT}^{j}}$. For the base case we initially have that ${{\mathcal{O}}_{\rm SAT}^{0}}$ is empty therefore our hypothesis applies. For the induction step we make a case distinction according to the rule that was applied to add $\langle \top \sqsubseteq\exists r.D,d\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$.

(CR1):

This implies that there exist subsumptions of the form $\langle{\top}\sqsubseteq{C^{\prime}},{d_1}\rangle\in{{\mathcal{O}}_{\rm SAT}^{j}}$, $\langle{C^{\prime}}\sqsubseteq{D},{d_2}\rangle\in{\mathcal{O}}$ and the rule adds $\langle{\top}\sqsubseteq{D},{\min(d_1,d_2)}\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. By IH we have that $\langle{C}\sqsubseteq{C^{\prime}},{d_1^{\prime}}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ for all $C\in BC_{\mathcal{O}}$ and some d ₁′ ≥ d ₁. Non applicability of Rule CR1 for $\langle{C}\sqsubseteq{C^{\prime}},{d_1^{\prime}}\rangle\in{{\mathcal{O}}_{\rm SAT}}$, $\langle{C^{\prime}}\sqsubseteq{D},{d_2}\rangle\in{\mathcal{O}}$ ensures that $\langle{C}\sqsubseteq{D},{d^{\prime}}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ for some d′ ≥ min (d ₁′,d ₂) ≥ min (d ₁,d ₂).

(CR7):

This implies that there exist subsumptions of the form $\langle{\top}\sqsubseteq{p_1(\overline{F}_1)},{d_1}\rangle,\ldots,\langle{\top}\sqsubseteq{p_m(\overline{F}_m)},{d_m}\rangle\in{{\mathcal{O}}_{\rm SAT}^{j}}$, and the conjunction ${{\bigwedge_{i=1}^m}}p_{i}\big(\overline{F}_{i}\big)\geq d_{i}$ is unsatisfiable and the rule adds $\langle{\top}\sqsubseteq{\bot},{1}\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. By IH we have that there exist subsumptions of the form $\langle{C}\sqsubseteq{p_1(\overline{F}_1)},{d_1^{\prime}}\rangle,\ldots,\langle{C}\sqsubseteq{p_m(\overline{F}_m)},{d_m^{\prime}}\rangle\in{{\mathcal{O}}_{\rm SAT}^{j}}$ with d _i ′ ≥ d _i . Non applicability of Rule CR7 for the latest subsumptions along with the unsatisfiability of the conjunction ${{\bigwedge_{i=1}^m}}p_{i}\big(\overline{F}_{i}\big)\geq d_{i}^{\prime}$ ensure that $\langle{C}\sqsubseteq{\bot},{1}\rangle\in{{\mathcal{O}}_{\rm SAT}}$.

(CR8a):

This implies that there exist subsumptions of the form $\langle{\top}\sqsubseteq{p_1(\overline{F}_1)},{d_1}\rangle,\ldots,\langle{\top}\sqsubseteq{p_m(\overline{F}_m)},{d_m}\rangle\in{{\mathcal{O}}_{\rm SAT}^{j}}$, and ${{\bigwedge}^m_{i=1}}p_{i}\big(\overline{F}_{i}\big)\geq d_{i}\models p \big(\overline{F}\big)\geq d$ and the rule adds adds $\langle{\top}\sqsubseteq{p(\overline{F})},{d}\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. By IH we have that there exist subsumptions of the form $\langle{C}\sqsubseteq{p_1(\overline{F}_1)},{d_1^{\prime}}\rangle,\ldots,\langle{C}\sqsubseteq{p_m(\overline{F}_m)},{d_m^{\prime}}\rangle\in{{\mathcal{O}}_{\rm SAT}^{j}}$ with d _i ′ ≥ d _i . Moreover, by the semantics of concrete domains we have that ${{\bigwedge}^m_{i=1}}p_{i}\big(\overline{F}_{i}\big)\geq d_{i}^{\prime}\models p\big(\overline{F}\big)\geq d$. Therefore, non applicability of rule CR8a ensures that $\langle{C}\sqsubseteq{p( \overline F)},{d^{\prime}}\rangle\in {{\mathcal{O}}_{\rm SAT}}$ for some d′ ≥ d.

(CR8b):

This rule never adds a concept subsumption of the form $\langle{\top}\sqsubseteq{D},{d}\rangle$ to ${{\mathcal{O}}_{\rm SAT}}$, therefore there is no need to examine it.

(CR9):

The proof of this rule is similar to the proof of rule $\textbf{CR7}$.

(Other Cases):

All the other cases can proved similar to case CR1.□

Proof of Theorem 1

(Completeness) Completeness is the only if direction of Theorem 1. We want to show that ${\mathcal{O}}\models \langle{\{o\}}\sqsubseteq{B},{d}\rangle$ implies that either Condition S1 or Condition S2 apply. It suffices to show that if Condition S2 does not apply, then ${\mathcal{O}}\models \langle{\{o\}}\sqsubseteq{B},{d}\rangle$ implies that Condition S1 applies.

Step 1.

We proceed in the standard way, defining a so-called canonical model (Baader et al. 2005) for which the above holds. Suppose that the saturation rules in Table 7 cannot be further applied and let $BC_{{\mathcal{O}}}^{-}$ be the following set:

$$ \begin{array}{cl} BC_{{\mathcal{O}}}^{-}:= & \big\{ C\mid \langle \{a\} \rightsquigarrow C,d^{\prime\prime} \rangle \in{{\mathcal{O}}_{\rm SAT}}\vphantom{x^{2^{2}}} \mbox{ for } \{a\} ,C\in BC_{{\mathcal{O}}} \mbox{ and } d^{\prime\prime}>0\vphantom{x^{2^{2}}}\big\} \end{array} $$

We inductively define the relation ~ on $BC_{{\mathcal{O}}}^{-}$ as follows:

$$ \begin{array}{rll} C\sim D\textnormal{ if\/f } \textnormal{ either } & \langle{C}\sqsubseteq{\{a\}},{1}\rangle, \langle{D}\sqsubseteq{\{a\}},{1}\rangle \in{{\mathcal{O}}_{\rm SAT}}\textnormal{ for some }\{a\} \in BC_{{\mathcal{O}}}\\ \par \textnormal{ or } & C=D \end{array}$$

It can be easily verified that ~ is an equivalence relation, while [C] = { D|C~D} is the equivalence class of some $C\in BC_{{\mathcal{O}}}^{-}$.

Proposition 4

Suppose that $\{a\},C\in BC_{\mathcal{O}}$ belong to the same equivalence class {a},C ∈ [E]. If $\langle{\{a\}}\sqsubseteq{F},{d}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ then $\langle{C}\sqsubseteq{F},{d^{\prime}}\rangle \in{{\mathcal{O}}_{\rm SAT}}$ for some d′ ≥ d.

Proof

Since {a},C ∈ [E] then there exists some nominal {b} such that $\langle{\{a\}}\sqsubseteq{\{b\}},{1}\rangle,\langle{C}\sqsubseteq{\{b\}},{1}\rangle\in{{\mathcal{O}}_{\rm SAT}}$.

If F is some concept in $BC_{\mathcal{O}}$. Since $\langle{C}\sqsubseteq{\{b\}},{1}\rangle, \langle{\{a\}}\sqsubseteq{\{b\}},{1}\rangle , \langle{\{a\}}\sqsubseteq{F},{d}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ and $\langle \{a\} \rightsquigarrow \{a\} ,1\rangle$ non applicability of rule CR6 ensures that $\langle{C}\sqsubseteq{F},{d^{\prime}}\rangle \in{{\mathcal{O}}_{\rm SAT}}$ for some d′ ≥ d.

If F is some concept description of the form $\exists r.D$ where $r\in R_{\mathcal{O}}$ and $D\in BC_{\mathcal{O}}$. Suppose that our algorithm is performed on m steps and the saturated ontology on step j is denoted with ${{\mathcal{O}}_{\rm SAT}^{j}}$ (we will use ${{\mathcal{O}}_{\rm SAT}}$ as a shortcut for ${{\mathcal{O}}_{\rm SAT}^{m}}$). We prove this by induction on the smallest j such that $\langle{\{a\}}\sqsubseteq{\exists r.D},{d}\rangle\in {{\mathcal{O}}_{\rm SAT}^{j+1}}\setminus{{\mathcal{O}}_{\rm SAT}^{j}}$. For the base case we initially have that ${{\mathcal{O}}_{\rm SAT}^{0}}$ is empty therefore our hypothesis applies. For the induction step we make a case distinction according to the rule that was applied to add $\langle \{a\} \sqsubseteq\exists r.D,d\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$.

(CR3):

This implies that there exists a subsumption of the form $\langle{\{a\}}\sqsubseteq{C^{\prime}},{d_1}\rangle\in$ ${{\mathcal{O}}_{\rm SAT}^{j}}$, and $\langle{C^{\prime}}\sqsubseteq{\exists r.D},{d_2}\rangle\in{\mathcal{O}}$ and the rule adds $\langle{\{a\}}\sqsubseteq{C^{\prime}},{\min(d_1,d_2)}\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. Since {a} ∈ [C], we have proved that $\langle{C}\sqsubseteq{C^{\prime}},{d_1^{\prime}}\rangle \in{{\mathcal{O}}_{\rm SAT}}$ for some d ₁′ ≥ d ₁. The latest along with $\langle{C^{\prime}}\sqsubseteq{\exists r.D},{d_2}\rangle\in{\mathcal{O}}$ and non applicability of rule CR3 ensure that $\langle C\sqsubseteq\exists r.D,d^{\prime}\rangle \in{{\mathcal{O}}_{\rm SAT}}$ for some d′ ≥ min (d ₁′,d ₂) ≥ min (d ₁,d ₂).

(CR10):

This implies that there exists a subsumption of the form $\langle{\{a\}}\sqsubseteq{\exists r.D},{d}\rangle\in$ ${{\mathcal{O}}_{\rm SAT}^{j}}$, and $r\sqsubseteq s\in{\mathcal{O}}$ and the rule adds $\langle{\{a\}}\sqsubseteq{\exists s. D},{ d}\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. Since {a} ∈ [C], by IH we also must have that $\langle{C}\sqsubseteq{\exists r.D},{d^{\prime}}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ for some d′ ≥ d. The latest along with $r\sqsubseteq s\in{\mathcal{O}}$ and non applicability of rule CR10 ensure that $\langle{C}\sqsubseteq{\exists s.D},{d^{\prime\prime}}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ for some d′′ ≥ d′ ≥ d.

(CR11):

This implies that there exist subsumptions of the form $\langle{\{a\}}\sqsubseteq{\exists r_1.D},{d_1}\rangle,$ $\langle{D}\sqsubseteq{\exists r_2.E},{d_2}\rangle\in{{\mathcal{O}}_{\rm SAT}^{j}}$, and $r_1\circ r_2\in{\mathcal{O}}$ and the rule adds $\langle{\{a\}}\sqsubseteq{\exists s.D},{\min(d_1,d_2)}\rangle$ to ${{\mathcal{O}}_{\rm SAT}^{j+1}}$. Since {a} ∈ [C], by IH we also must have that $\langle{C}\sqsubseteq{\exists r_1.D},{d_1^{\prime}}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ for some d ₁′ ≥ d ₁. The latest along with $\langle{D}\sqsubseteq{\exists r_2.E},{d_2}\rangle\in{{\mathcal{O}}_{\rm SAT}^{j}}$, $r\sqsubseteq s\in{\mathcal{O}}$, and non applicability of rule CR11 ensure that $\langle{C}\sqsubseteq{\exists s.D},{d^{\prime}}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ for some d′ ≥ min (d ₁′,d ₂) ≥ min (d ₁,d ₂).□

Step 2.

For each concept $C\in BC_{{\mathcal{O}}}$ and a concrete domain ${\mathcal{D}}$, we build the conjunction ${\textnormal{conj}}_{C,{\mathcal{D}}}$ as follows:

$$ {\textnormal{conj}}_{C,{\mathcal{D}}}:=\bigwedge\limits_{\langle C\sqsubseteq{p(\overline{F})},d\rangle\in{{\mathcal{O}}_{\rm SAT}}\textnormal{ and }p\in\Phi^{{\mathcal{D}}}}p(\overline{F})\geq d. $$

That is ${\textnormal{conj}}_{C,{\mathcal{D}}}$ is constructed from all the fuzzy concept inclusions in ${{\mathcal{O}}_{\rm SAT}}$ that have C in the left and a concrete domain predicate $p\in\Phi^{\mathcal{D}}$ on the right. A thresholded, by some degree d _thr ∈ (0,1], form of ${\textnormal{conj}}_{C,{\mathcal{D}}}$ can be built as follows:

$$ {\textnormal{conj}}_{C,{\mathcal{D}},d_{\rm thr}}:=\bigwedge\limits_{\langle C\sqsubseteq{p(\overline{F})},d\rangle\in{{\mathcal{O}}_{\rm SAT}}\textnormal{ and }p\in\Phi^{{\mathcal{D}}}}p(\overline{F})\geq \min(d,d_{\rm thr}). $$

We will now prove that for every $C\in BC_{{\mathcal{O}}}^{-}$ and threshold d _thr there exists a solution δ for ${\textnormal{conj}}_{C,{\mathcal{D}},d_{\rm thr}}\wedge {\textnormal{conj}}_{\top,{\mathcal{D}}}$ that satisfies certain properties. This solution will later be used in order to define a link between feature names and the concrete domain in the interpretation $\mathcal{I}$ that we are going to build.

Proposition 5

For each $C\in BC_{{\mathcal{O}}}^{-}$ , each strict fuzzy p-admissible concrete domain $\mathcal{D}$ , and threshold degree d _thr ∈ (0,1], there exists a solution δ for ${\textnormal{conj}}_{C,{\mathcal{D}},d_{\rm thr}}\wedge {\textnormal{conj}}_{\top,{\mathcal{D}}}$ such that: $\delta\models p(\overline{F})=d$ if $p(\overline{F})\geq d$ appears in ${\textnormal{conj}}_{C,{\mathcal{D}},d_{\rm thr}}\wedge {\textnormal{conj}}_{\top,{\mathcal{D}}}$ . We will use the shortcut $\delta_{C,{\mathcal{D}},d_{\rm thr}}$ for the specific solution.

Proof

By not satisfaction of Condition S2 we have that $\langle{\{a\} }\sqsubseteq{\bot},0\rangle$ for each $\{a\} \in BC_{{\mathcal{O}}}^{-}$. By definition of $BC_{{\mathcal{O}}}^{-}$ and non applicability of Rule CR5 we have that $\langle C\sqsubseteq{\bot},0\rangle\in{{\mathcal{O}}_{\rm SAT}}$ for each $C\in BC_{{\mathcal{O}}}^{-}$. Thus rule CR7 ensures that there exists at least one solution δ satisfying the conjunction ${\textnormal{conj}}_{C,{\mathcal{D}}}.$

Proposition 3 ensures that each conjunct in ${\textnormal{conj}}_{\top,{\mathcal{D}}}$ also appears in ${\textnormal{conj}}_{C,{\mathcal{D}}}$ with a greater degree. Therefore and since there exists a solution for ${\textnormal{conj}}_{C,{\mathcal{D}}}$, there also exists a solution for ${\textnormal{conj}}_{C,{\mathcal{D}}}\wedge {\textnormal{conj}}_{\top,D}$. Since ${\textnormal{conj}}_{C,{\mathcal{D}},d_{\rm thr}}\wedge {\textnormal{conj}}_{\top,{\mathcal{D}}}$ is more general than ${\textnormal{conj}}_{C,{\mathcal{D}}}\wedge {\textnormal{conj}}_{\top,D}$ we have that there also exists at least one solution for ${\textnormal{conj}}_{C,{\mathcal{D}},d_{\rm thr}}\wedge {\textnormal{conj}}_{\top,{\mathcal{D}}}$.

We make the hypothesis that the Proposition does not apply. Suppose that the previous conjunction has n solutions each one denoted as δ _λ with 1 ≤ λ ≤ n. Since the Proposition does not apply, for every solution δ _λ there exists some $p_{\lambda}(\overline{F}_{\lambda})$ such that (i) $\delta_{\lambda}\models p_{\lambda}(\overline{F}_{\lambda})=d_{\lambda}$ and (ii) $p_{\lambda}(\overline{F}_{\lambda})\geq d_{\lambda}$ does not appear in ${\textnormal{conj}}_{C,{\mathcal{D}},d_{\rm thr}}\wedge {\textnormal{conj}}_{\top,{\mathcal{D}}}$. The latest implies that

$$ {\textnormal{conj}}_{C,{\mathcal{D}},d_{\rm thr}}\wedge {\textnormal{conj}}_{\top,{\mathcal{D}}}\models\underset{1\leq\lambda\leq n}{\bigvee}p_{\lambda}(\overline{F}_{\lambda})\geq d_{\lambda} $$

and Property 2 of Definition 1 (loose fuzzy p-admissible concrete domains) ensures that ${\textnormal{conj}}_{C,{\mathcal{D}},d_{\rm thr}}\wedge {\textnormal{conj}}_{\top,{\mathcal{D}}}\models p_{\lambda}(\overline{F}_{\lambda})\geq d_{\lambda}$ for some 1 ≤ λ ≤ n.

We will consider the cases for d _λ  > d _thr and for d _λ  ≤ d _thr. For the first case, since d _λ  > d _thr, based on Property 4 of Definition 2 we conclude that ${\textnormal{conj}}_{\top,{\mathcal{D}}}\models p_{\lambda}(\overline{F}_{\lambda})\geq d_{\lambda}$ and non applicability of rule CR8a ensures that $p_{\lambda}(\overline{F}_{\lambda})\geq d_{\lambda}$ appears in ${\textnormal{conj}}_{\top,{\mathcal{D}}}$.

For the second case, the fact that d _λ  ≤ d _thr along with Property 1 of Definition 2 ensure that ${\textnormal{conj}}_{C,{\mathcal{D}},d_{\rm thr}}\wedge {\textnormal{conj}}_{\top,{\mathcal{D}},d_{\rm thr}}\models p_{\lambda}(\overline{F}_{\lambda})\geq d_{\lambda}$. The latest implication along with Proposition 3 ensure that ${\textnormal{conj}}_{C,{\mathcal{D}},d_{\rm thr}}\models p_{\lambda}(\overline{F}_{\lambda})\geq d_{\lambda}$ implying by the semantics of fuzzy concrete domains ${\textnormal{conj}}_{C,{\mathcal{D}}}\models p_{\lambda}(\overline{F}_{\lambda})\geq d_{\lambda}$. The latest along with non applicability or rule CR8a ensures that $p_{\lambda}(\overline{F}_{\lambda})\geq d_{\lambda}^{\prime}$ appears in ${\textnormal{conj}}_{C,{\mathcal{D}}}$ for some d _λ ′ ≥ d _λ and Property 1 of Definition 2 ensures that $p_{\lambda}(\overline{F}_{\lambda})\geq d_{\lambda}$.

In both cases $p_{\lambda}(\overline{F}_{\lambda})\geq d_{\lambda}$ appears in ${\textnormal{conj}}_{C,{\mathcal{D}},d_{\rm thr}}\wedge {\textnormal{conj}}_{\top,{\mathcal{D}}}$ and therefore the hypothesis we have made is wrong and the proof has finished.□

Proposition 6

For each nominal $\{a\}\in BC_{{\mathcal{O}}}^{-}$ and each (loose or strict) fuzzy p-admissible concrete domain $\mathcal{D}$ , there exists a solution δ for ${\textnormal{conj}}_{\{a\},{\mathcal{D}}}$ such that: $\delta\models p(\overline{F})=d$ if $p(\overline{F})\geq d$ appears in ${\textnormal{conj}}_{\{a\},{\mathcal{D}}}$ . We will use the shortcut $\delta_{\{a\},{\mathcal{D}}}$ for the specific solution.

The proof can be performed similar to the previous proof.

Step 3.

We will now proceed to define a fuzzy interpretation $\mathcal{I}$. We will later show that this interpretation is also a model for ${\mathcal{O}}$.

For the rest of the proof, for every $C \in BC_{\mathcal{O}}^{-}$, concept description D, and $r\in R_{\mathcal{O}}$, we will use the degrees d _C , $d_{C\sqsubseteq D}$, d _r(C,D) as shortcuts for

$$\begin{array}{rll} d_C&=&\sup\{d\mid \langle \{a\} \rightsquigarrow C ,d \rangle \textnormal{ and }\{a\}\in BC_C \}\\ d_{C\sqsubseteq D}&=&d \textnormal{\ \ if }\langle{C}\sqsubseteq{D},{d}\rangle\in{{\mathcal{O}}_{\rm SAT}} \\ d_{r(C,D)}&=& \sup\{d\mid \langle{C}\sqsubseteq{\exists r.D^{\prime}},{d}\rangle\in{{\mathcal{O}}_{\rm SAT}} \textnormal{ and }D^{\prime} \in [D]\} . \end{array}$$

For the previous use of shortcuts, in case that $\langle{C}\sqsubseteq{F},{d}\rangle$ does not appear in ${{\mathcal{O}}_{\rm SAT}}$ for any degree d, we will assume that $\langle{C}\sqsubseteq{F},{0}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ for every concept $F\in BC_{\mathcal{O}}$ or concept description $F=\exists r.D$ where $D\in BC_{\mathcal{O}}$.

We define a fuzzy interpretation $\mathcal{I}$ as follows (where $A\in BC_{{\mathcal{O}}}$ is a concept name, $D,D^{\prime}\in BC_{{\mathcal{O}}}$, r is a role name in $R_{{\mathcal{O}}}$, {a} is a nominal in $BC_{{\mathcal{O}}}$, and $C\in BC_{{\mathcal{O}}}^-$):

$$ \begin{array}{rll} \Delta^{\mathcal{I}} & := \big\{ [C]\mid C\in BC_{{\mathcal{O}}}^{-}\big\} \\ a^{\mathcal{I}} & :=[\{a\} ]\\ A^{\mathcal{I}}([C]) & := \begin{cases} d_{\{a\}\sqsubseteq A} \quad\textnormal{if there exists some }\{a\} \in[C]\\ \max(\min(d_{C \sqsubseteq A},d_C),d_{\top \sqsubseteq A} ) \quad\textnormal{otherwise} \end{cases}\\ r^{\mathcal{I}}([C],[D]) & := \begin{cases} d_{r(\{a\},D)} \quad\textnormal{if there exists some }\{a\} \in[C]\\ \max(\min(d_{r(C,D)},d_{C}),d_{r(\top,D)}) \quad\textnormal{otherwise}\\ \end{cases}\\ f^{\mathcal{I}}([C]) & := \begin{cases} \delta_{\{a\},{\mathcal{D}}}(f) \quad(i)\textnormal{ there exists some }\{a\} \in[C],\\ \quad(ii)\textnormal{ }\langle{\{a\}}\sqsubseteq{p(\overline{F})},{d}\rangle\in{{\mathcal{O}}_{\rm SAT}}\textnormal{ for some }d>0,\\ \quad\hphantom{(ii)} f \textnormal{ appears in }\overline{F}\textnormal{, and }p\in\Phi^{\mathcal{D}}.\\ \delta_{C,{\mathcal{D}},d_C}(f) \quad(i)\textnormal{ there exists no }\{a\} \in[C],\\ \quad(ii)\textnormal{ }\langle{C}\sqsubseteq{p(\overline{F})},{d}\rangle\in{{\mathcal{O}}_{\rm SAT}}\textnormal{ for some }d>0,\\ \quad\hphantom{(ii)} f \textnormal{ appears in }\overline{F} \textnormal{, and }p\in\Phi^{\mathcal{D}}.\\ \end{cases}\\ \end{array} $$

where the mappings $\delta_{\{a\},{\mathcal{D}}}$, $\delta_{C,{\mathcal{D}},d_C}$ are defined according to Propositions 5 and 6.

Since ~ is an equivalence relation each nominal {a} belongs to exactly one equality class, therefore $a^\mathcal{I}$ is uniquely defined. Moreover Proposition 4 ensures that each concept, role, and feature name interpretation is uniquely defined. Therefore the intepretation $\mathcal{I}$ is well defined.

Proposition 7

For all $[C]\in\Delta^{\mathcal{I}}$ and $D\in BC_{{\mathcal{O}}}\cup\{ \bot\}$ , we have that $D^{\mathcal{I}}([C])=d$ iff one of the following two conditions holds:

• T1 There exists some nominal {a} ∈ [C] and $d=d_{\{a\} \sqsubseteq D}$,

• T2 There exists no nominal in [C] and $d={\max(\min(d_{C \sqsubseteq D},d_{C}),d_{\top \sqsubseteq D})}.$

Proof

We make a case distinction regarding the type of D:

D is the top concept $(D=\top)$

For every $[C]\in\Delta^{\mathcal{I}}$ we have that$\top^{\mathcal{I}}([C])=1$ by the semantics of the top concept. Since $\langle \top\sqsubseteq\top,1\rangle \in{{\mathcal{O}}_{\rm SAT}}$ and $\langle \{a\} \sqsubseteq\top,1\rangle \in{{\mathcal{O}}_{\rm SAT}}$ for every $\{a\} \in BC_{{\mathcal{O}}}$ Conditions T1 and T2 trivially apply.

D is the bottom concept $(D=\bot)$

For every $[C]\in\Delta^{\mathcal{I}}$ we have that $\bot^{\mathcal{I}}([C])=0$ by the semantics of the bottom concept. By not satisfaction of Condition S2 we have that $\langle{ \{a\}}\sqsubseteq{\bot},{0}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ for each nominal $\{a\} \in BC_{{\mathcal{O}}}$, i.e. $d_{\{a\},\bot}=0$. Since $\langle{ \{a\}}\sqsubseteq{\bot},{0}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ for each nominal $\{a\} \in BC_{{\mathcal{O}}}$, due to Rule CR5 and by construction of $BC_{{\mathcal{O}}}^{-}$, it follows that $\langle C\sqsubseteq\bot,0\rangle\in{{\mathcal{O}}_{\rm SAT}}$, i.e. $d_{C\sqsubseteq \bot}=0$, for all $C \in BC_{{\mathcal{O}}}^{-}$. Therefore $d_{\{a\}\sqsubseteq \bot}=d_{C\sqsubseteq D}= d_{\top\sqsubseteq \bot}=0$ and Conditions T1 and T2 apply.

D is a concept name (D = A)

Then the two Conditions apply by construction of $A^{\mathcal{I}}$.

D is some nominal (D = {c})

Rule CR12 ensures that $d_{C\sqsubseteq \{a\}}$ is either 0 or 1 for every concept C and nominal {a}.

For the if direction. Suppose that $d_{\{a\}\sqsubseteq \{c\}}=1$ for some nominal {a} ∈ [C]. It remains to prove that $\{c\} ^{\mathcal{I}}([C])=1$. By definition of the [C] equivalence class we have that [{c} ] = [{a}] = [C]. Since, by construction of $\mathcal{I}$, $c^{\mathcal{I}}=[\{c\} ]=[C]$ we have that $\{c\} ^{\mathcal{I}}([C])=1$. In a similar way we prove that if $\langle \{a\} \sqsubseteq\{c\} ,0\rangle\in{{\mathcal{O}}_{\rm SAT}}$ then $\{c\} ^{\mathcal{I}}([C])=0$.

For the only if direction. Suppose that $\{c\} ^{\mathcal{I}}([C])=1$, it remains to prove that $\langle \{a\} \sqsubseteq\{c\} ,1\rangle$ for all {a} ∈ [C]. Since $\{c\} ^{\mathcal{I}}([C])=1$ by construction of $\mathcal{I}$ we have that $c^{\mathcal{I}}=[C]$, i.e. {c} ∈ [C], and according to Proposition 4 we have that $\langle \{a\} \sqsubseteq\{c\} ,1\rangle$, i.e. $d_{\{a\}\sqsubseteq \{c\}}=1$. In a similar way we prove that if $\{c\} ^{\mathcal{I}}([C])=0$ then $\langle \{a\} \sqsubseteq\{c\} ,0\rangle$ for all {a} ∈ [C].

In case that there exists no nominal in [C] it is easy to prove that $\langle C \sqsubseteq \{c\} ,0\rangle \in{{\mathcal{O}}_{\rm SAT}}$ and $\{c\} ^{\mathcal{I}}([C])=0$.

D is some concrete domain predicate $(D=p(\overline{F}))$

For every $[C]\in\Delta^\mathcal{I}$ and concrete domain ${\mathcal{D}}^\mathcal{I}$ we have that $p(\overline{F})^{\mathcal{I}}([C])=d$ iff $p^{\mathcal{D}}(\overline{F}^{\mathcal{I}}([C]))=d$.

If there exists some nominal {a} ∈ [C] then by construction of the interpretation of $\overline{F}^{\mathcal{I}}([C])$ we have that the previous equality is satisfied iff $p^{\mathcal{D}}(\delta_{\{a\},{\mathcal{D}}}(\overline{F}))=d$ where $\delta_{\{a\},{\mathcal{D}}}$ corresponds to the solution presented in Proposition 6. By choice of the solution, the latest applies iff $\langle{\{a\} }\sqsubseteq{p(\overline{F})},d\rangle\in{{\mathcal{O}}_{\rm SAT}}$, i.e. $d_{\{a\}\sqsubseteq p(\overline{F})}=d$. Therefore Condition 1 applies.

If there exists no nominal in [C] then by construction of the interpretation of $\overline{F}^{\mathcal{I}}([C])$ we have that the previous Equality is satisfied iff $p^{\mathcal{D}}(\delta_{C,{\mathcal{D}},d_C}(\overline{F}))=d$ where $\delta_{C,{\mathcal{D}},d_C}$ corresponds to the solution presented in Proposition 5. By choice of the $\delta_{C,{\mathcal{D}},d_C}$ solution, the latest applies iff $p(\overline{F})\geq d$ appears in ${\textnormal{conj}}_{C,{\mathcal{D}},d_C}\wedge {\textnormal{conj}}_{\top,{\mathcal{D}}}$. By construction of the two conjunctions, $p(\overline{F})\geq d$ appears in ${\textnormal{conj}}_{C,{\mathcal{D}},d_C}$ when $d=\min\big(d_{C\sqsubseteq p(\overline{F})},d_C\big)$ and $p(\overline{F})\geq d$ appears in ${\textnormal{conj}}_{\top,{\mathcal{D}}}$ when $d=d_{\top\sqsubseteq p(\overline{F})}$. Therefore $p(\overline{F})\geq d$ appears in ${\textnormal{conj}}_{C,{\mathcal{D}},d_C}\wedge {\textnormal{conj}}_{\top,{\mathcal{D}}}$ iff $d=\max\big(\min\big(d_{C\sqsubseteq p(\overline{F})},d_C\big),d_{\top\sqsubseteq p(\overline{F})}\big)$. Therefore Condition 2 applies.□

Step 4.

We now show that the constructed interpretation $\mathcal{I}$ is a model of ${\mathcal{O}}$, i.e. each concept and role inclusion in ${\mathcal{O}}$ is satisfied in $\mathcal{I}$. We make a case distinction according to the form of each concept and role inclusions in ${\mathcal{O}}$:

$\langle C^{\prime}\sqsubseteq D,d\rangle$ :

Suppose that $C^{{\prime}I}([C])= e$. It suffices to show that $D^\mathcal{I}([C]\geq \min(e,d)$.

If there exists no nominal in [C] then $e={\max(\min(d_{C \sqsubseteq C^{\prime}},d_{C}),d_{\top \sqsubseteq C^{\prime}})}$ according to Proposition 7. Non applicability of rule CR1 for ${\langle{C}\sqsubseteq{C^{\prime}},{d_{C\sqsubseteq C^{\prime}}}}\rangle\in{{\mathcal{O}}_{\rm SAT}}$, $\langle{C^{\prime}}\sqsubseteq{D},{d}\rangle\in{\mathcal{O}}$ ensures that $d_{C \sqsubseteq D}\geq\min(d_{C \sqsubseteq C^{\prime}},d)$. Non applicability of rule CR1 also ensures that $d_{\top \sqsubseteq D}\geq\min(d_{\top \sqsubseteq C^{\prime}},d)$. By Proposition 7 and the previous inequalities:

$$ D^{\mathcal{I}}([C])={\max(\min(d_{C \sqsubseteq D},d_{C}),d_{\top \sqsubseteq D})}\geq\min(e,d). $$

If there exists some {a} ∈ [C] then $e=d_{\{a\} \sqsubseteq C^{\prime}}$ according to Proposition 7. Non applicability of rule CR1 ensures that $d_{\{a\} \sqsubseteq D}\geq\min(d_{\{a\} \sqsubseteq C^{\prime}},d)=\min(e,d)$. By Proposition 7 and the previous inequality:

$$ D^{\mathcal{I}}([C])=d_{\{a\} \sqsubseteq D} \geq \min(e,d). $$

$\langle C_{1}\sqcap C_{2}\sqsubseteq D,d\rangle$ :

Suppose that $(C_{1}\sqcap C_{2})^{\mathcal{I}}([C])=e$. The latest implies that $C_1^\mathcal{I}([C])=e_1\geq e$, $C_2^\mathcal{I}([C])=e_2 \geq e$. It suffices to show that $D^\mathcal{I}([C])\geq\min(e,d)$.

If there exists no nominal in [C] then according to Proposition 7 we have that $e_1= {\max(\min(d_{C \sqsubseteq C_1},d_{C}),d_{\top \sqsubseteq C_1})}$ and $e_2= {\max(\min(d_{C \sqsubseteq C_2},d_{C}),d_{\top \sqsubseteq C_2})}$. Non applicability of rule CR2 ensures that $d_{C\sqsubseteq D}\geq \min(d_{C\sqsubseteq C_1},d_{C\sqsubseteq C_2},d)$ and that $d_{\top\sqsubseteq D}\geq \min(d_{\top\sqsubseteq C_1},d_{\top\sqsubseteq C_2},d)$. By Proposition 7 and the previous inequalities we have that

$$ D^{\mathcal{I}}([C])={\max(\min(d_{C \sqsubseteq D},d_{C}),d_{\top \sqsubseteq D})} \geq \min(e,d). $$

If there exists some nominal in [C] the proof can be performed similarly.

$\langle C^{\prime}\sqsubseteq\exists r.D,d\rangle$ :

Suppose that $C^{\prime I}([C])= e$. It suffices to show that $(\exists r.D)^\mathcal{I}([C])\geq \min(e,d)$, i.e. there exists some $x\in\Delta^\mathcal{I}$ such that $r^\mathcal{I}([C],x)\geq\min(e,d)$ and $D^\mathcal{I}(x)\geq\min(e,d)$.

If there exists no nominal in [C] then $e={\max(\min(d_{C \sqsubseteq C^{\prime}},d_{C}),d_{\top \sqsubseteq C^{\prime}})}$ according to Proposition 7. Non applicability of rule CR3 ensures that $d_{C\sqsubseteq\exists r. D}\geq\min(d_{C\sqsubseteq C^{\prime}},d)$ and $d_{\top\sqsubseteq\exists r. D}\geq\min(d_{\top\sqsubseteq C^{\prime}},d)$. By definition of the d _{r(C, D)}, $d_{r(\top, D)}$ degrees and the previous inequalities we have that

$$\begin{array}{rll} d_{r(C,D)}&\geq& d_{C\sqsubseteq\exists r.D}\geq \min(d_{C\sqsubseteq C^{\prime}},d)\\ d_{r(\top,D)}&\geq&d_{\top\sqsubseteq\exists r.D}\geq \min(d_{\top\sqsubseteq C^{\prime}},d) \end{array}$$

Finally by construction of $r^\mathcal{I}$ and the previous inequalities we have that

$$\begin{array}{rll} r^\mathcal{I}([C],[D])&=&\max(\min(d_{r(C,D)},d_{C}),d_{r(\top,D)})\geq\\ &\geq&\max(\min(d_{C\sqsubseteq C^{\prime}},d_C,d),\min(d_{\top\sqsubseteq C^{\prime}},d))\geq\min(e,d) \end{array}$$

(we consider that [D] appears in $\Delta^\mathcal{I}$ since as we will later prove d _D  > 0 and therefore $D\in BC^{-}_{\mathcal{O}}$). It remains to show that $D^\mathcal{I}([D])\geq\min(e,d)$. We will consider the following alternatives:

• (i) There exists no nominal in [D]. By the values of the d _C and the $d_{C\sqsubseteq \exists r.D}$ degrees, and by definition of the d _D degree, it is implied that $d_D\geq \min(d_C,d_{C\sqsubseteq \exists r.D})\geq \min(d_C,d_{C\sqsubseteq C^{\prime}},d)$. Proposition 3 ensures that $d_D\geq d_{\top\sqsubseteq\exists r. D}.$ Therefore

  $$ d_D\geq \max(\min(d_C,d_{C\sqsubseteq C^{\prime}},d), d_{\top\sqsubseteq \exists r.D})\geq \min(e,d) $$

  and since $d_{D\sqsubseteq D}=1$ we conclude that $D^\mathcal{I}([D])\geq\min(e,d).$

• (ii) There exists some nominal {a} ∈ [D]. In that case $D^\mathcal{I}([D])=d_{\{a\}\sqsubseteq D}$. Similarly to the previous alternative we can show that d _D  ≥ min (e,d) and therefore there exists some nominal {b} such that $\langle \{b\} \rightsquigarrow D ,\min(e,d)\rangle$. Since {a} ∈ [D], then according to Proposition 4 we also have that $\langle{D}\sqsubseteq{\{a\}},{1}\rangle \in {{\mathcal{O}}_{\rm SAT}}$. Non applicability of rule CR6 for $\langle{\{a\}}\sqsubseteq{\{a\}},{1}\rangle$, $\langle{D}\sqsubseteq{\{a\}},{1}\rangle \in {{\mathcal{O}}_{\rm SAT}}$, $\langle \{b\} \rightsquigarrow D,$ $\min(e,d)\rangle$, and $\langle{D}\sqsubseteq{D},{1}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ ensures that $d_{\{a\}\sqsubseteq D}\geq \min(e,d)$. Therefore $D^\mathcal{I}([D])\geq \min(e,d)$

If there exists some nominal in [C] the proof can be performed similarly.

$\langle \exists r.C^{\prime}\sqsubseteq D,d\rangle$ :

Suppose that $(\exists r.C^{\prime})^\mathcal{I}([C])= e$. By the semantics of existential restrictions we have that $r^\mathcal{I}([C],[E])\geq e$ and $C^{\prime I}([E])\geq e$ for some $[E]\in\Delta^\mathcal{I}$. It remains to show that $D^\mathcal{I}([C]\geq \min(e,d)$.

If there exists no nominal in [C] then, by construction of $r^\mathcal{I}([C],[E])$, we have that $r^\mathcal{I}([C],[E])=\max(\min(d_{r(C,E)},d_{C}),d_{r(\top,E)})\geq e$. We consider the following alternatives:

• (i) There exists no nominal in [E], d _r(C,E) ≥ e, and d _C  ≥ e. By definition of the d _r(C,E) degree and since only E ∈ [E] we have that $d_{C\sqsubseteq \exists r.E}\geq e$. Since $C^{\prime I}([E])\geq e$, Propositions 3 and 7 ensure that $d_{E\sqsubseteq C^{\prime}}\geq e$. Therefore non applicability of rule CR4 ensures that

  $$ d_{C\sqsubseteq D}\geq\min(d_{C\sqsubseteq \exists r.E},d_{E\sqsubseteq C^{\prime}},d)\geq \min(e,d) $$

  and according to Proposition 7 we have that

  $$ D^\mathcal{I}([C]) \geq \min(d_{C\sqsubseteq D},d_C)\geq \min(e,d). $$

• (ii) There exists no nominal in [E] and $d_{r(\top,E)}\geq e$. Working as for the previous point we prove that $d_{\top\sqsubseteq D}\geq \min(e,d)$ and according to Proposition 7 we have that

  $$D^\mathcal{I}([C])\geq d_{\top\sqsubseteq D}\geq \min(e,d).$$

• (iii) There exists some nominal {a} ∈ [E], d _r(C,E) ≥ e, and d _C  ≥ e. By definition of the d _r(C,E) degree we have that $d_{C\sqsubseteq \exists r.E^{\prime}}\geq e$ for some E′ ∈ [E]. Since $C^{\prime I}([E])\geq e$ Propositions 4 and 7 ensure that $d_{E^{\prime}\sqsubseteq C^{\prime}}\geq e$. Therefore non applicability of rule CR4 ensures that

  $$ d_{C\sqsubseteq D}\geq\min(d_{C\sqsubseteq \exists r.E^{\prime}},d_{E^{\prime}\sqsubseteq C^{\prime}},d)\geq \min(e,d). $$

  and since d _C  ≥ e, Proposition 7 ensures that

  $$ D^\mathcal{I}([C]) \geq\min(d_{C\sqsubseteq D},d_C) \geq\min(e,d). $$

• (iv) There exists some nominal {a} ∈ [E] and $d_{r(\top,E)}\geq e$. Working as for the previous point we prove that $d_{\top\sqsubseteq D}\geq \min(e,d)$ and by Proposition 7 we have that

  $$ D^\mathcal{I}([C])\geq d_{\top\sqsubseteq D}\geq \min(e,d). $$

If there exists some nominal in [C] the proof can be performed similarly.

$r\sqsubseteq s$ :

Suppose that $r^{\mathcal{I}}([C],[F])=e$ for some $[C],[F]\in\Delta^\mathcal{I}$. It remains to prove that $s^{\mathcal{I}}([C],[F])\geq e.$

If there exists no nominal in [C] then, by construction of $r^{\mathcal{I}}$, we have that either d _r(C,F) ≥ e and d _C  ≥ e or $d_{r(\top,F)}=e$. We will consider the following alternatives:

• (i) d _r(C,F) ≥ e and d _C  ≥ e. Then there exists some F′ ∈ [F] such that $d_{C\sqsubseteq\exists r.F^{\prime}}\geq e$. Non applicability of rule CR10 ensures that

  $$d_{C\sqsubseteq \exists s.F^{\prime}}\geq d_{C\sqsubseteq \exists r.F^{\prime}}\geq e.$$

  and by construction of $s^\mathcal{I}$ we have that

  $$ s^\mathcal{I}([C],[F])\geq\min(d_{s(C,F)},d_C) \geq \min(d_{C\sqsubseteq \exists s.F^{\prime}},e)\geq e.$$

• (ii) $d_{r(\top,F)}= e$. Working as for the previous point we prove that $d_{\top,\exists r.F^{\prime}}\geq e.$ Therefore by construction of $s^\mathcal{I}$ we have

  $$ s^\mathcal{I}([C],[F]) \geq d_{s(\top,F)} \geq d_{\top\sqsubseteq \exists r.F^{\prime}}\geq e $$

If there exists some nominal in [C] the proof can be performed similarly.

$r_{1}\circ r_{2}\sqsubseteq s$ :

Suppose that $r_{1}^{\mathcal{I}}([C],[D])=e_{1}$ and $r_{2}^{\mathcal{I}}([D],[F])=e_{2}$ for some $[C],[D],[F]\in\Delta^\mathcal{I}$. It suffices to show that $s^{\mathcal{I}}([C],[F])\geq\min(e_{1},e_{2})$.

If there exists no nominal in [C] then by construction of $r_1^\mathcal{I}$ we have that either $d_{r_1(C,D)}\geq e_1$ and d _C  ≥ e ₁, or $d_{r_1(\top,D)}=e_1$. We will consider the following alternatives:

• (i) If there exists no nominal in [D], $d_{r_1(C,D)}\geq e_1$, and d _C  ≥ e ₁. Since there exists no nominal in [D] then only D ∈ [D] and therefore $d_{r_1(C,D)}=d_{C\sqsubseteq \exists r_1.D}\geq e_1$. Since $r_2^\mathcal{I}([D],[F])=e_2$, by construction of $r_2^\mathcal{I}$ and Proposition 3 we have that $d_{r_2(D,F)}\geq e_2$ which implies that there exists some F′ ∈ [F] such that $d_{D\sqsubseteq \exists r_2.F^{\prime}}\geq e_2$. Non applicability of rule CR11 ensures that

  $$ d_{C\sqsubseteq \exists s.F^{\prime}}\geq \min(d_{C\sqsubseteq \exists r_1.D},d_{D\sqsubseteq \exists r_2.F^{\prime}}) \geq \min(e_1,e_2) $$

  Therefore by construction of $s^\mathcal{I}$:

  $$\begin{array}{rll} s^\mathcal{I}([C],[F]) &\geq& \min(d_{s(C,F)},d_C)\\ &\geq& \min(d_{C\sqsubseteq \exists s.F^{\prime}},e_1) \geq\min(e_1,e_2). \end{array}$$

• (ii) If there exists no nominal in [D] and $d_{r_1(\top,D)}\geq e_1$. Working as for the previous point we prove that $d_{\top\sqsubseteq \exists s.F^{\prime}}\geq \min(e_1,e_2)$ and by construction of $s^\mathcal{I}$:

  $$ s^\mathcal{I}([C],[F])\geq d_{s(\top,F)} \geq d_{\top\sqsubseteq \exists s.F^{\prime}} \geq\min(e_1,e_2). $$

• (iii) There exists some nominal {a} ∈ [D], $d_{r_1(C,D)}\geq e_1$, and d _C  ≥ e ₁. Then $d_{C\sqsubseteq \exists r_1.D^{\prime}}\geq e_1$ for some D′ ∈ [D]. Since $r_2^\mathcal{I}([D],[F])=e_2$ we have by construction of $r_2^\mathcal{I}$ that $d_{\{a\}\sqsubseteq\exists r_2 .F^{\prime}}=e_2$ and Proposition 4 ensures that $d_{D^{\prime}\sqsubseteq\exists r_2.F^{\prime}}\geq e_2$. Non applicability of rule CR11 ensures that:

  $$ d_{C\sqsubseteq \exists s. F^{\prime}}\geq \min(d_{C\sqsubseteq \exists r_1.D^{\prime}},d_{D^{\prime}\sqsubseteq \exists r_2.F^{\prime}})\geq \min(e_1,e_2). $$

  and by construction of $s^\mathcal{I}$ we have that

  $$\begin{array}{rll} s^\mathcal{I}([C],[F]) &\geq& \min(d_{s(C,F)},d_C) \\ &\geq& \min(d_{C\sqsubseteq \exists s.F^{\prime}},e_1) \geq\min(e_1,e_2). \end{array}$$

• (iv) There exists some nominal {a} ∈ [D] and $d_{r_1(\top,D)}\geq e_1$. Working as before we can show that $d_{\top\sqsubseteq \exists s. F^{\prime}}\geq\min(e_1,e_2)$ for some F′ ∈ [F] and therefore by construction of $s^\mathcal{I}$

  $$ s^\mathcal{I}([C],[F])\geq d_{s(\top,F)}\geq d_{\top\sqsubseteq \exists s.F^{\prime}} \geq\min(e_1,e_2). $$

If there exists some nominal in [C] the proof can be performed similarly.

Step 5.

We have proved that $\mathcal{I}$ is a model of ${\mathcal{O}}$. If ${\mathcal{O}} \models \langle{\{o\}}\sqsubseteq{B},{d}\rangle$, then for the interpretation $\mathcal{I}$ we have constructed, it applies that $B^\mathcal{I}(o^\mathcal{I})\geq d$. The latest along with Proposition 7 imply that $d_{\{o\}\sqsubseteq B}\geq d$, i.e. that $\langle{\{o\}}\sqsubseteq{B},{d^{\prime}}\rangle\in{{\mathcal{O}}_{\rm SAT}}$ for some d′ ≥ d as we wanted to prove.