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.

1 Introduction

Description Logics (DLs) are a class of knowledge representation languages with well-defined semantics and decidable reasoning algorithms which are widely used in a variety of knowledge-based applications on the Semantic Web (Baader et al. 2003). Unfortunately, there are occasions where classical DL formalisms fail to accurately represent the concepts that appear in a domain of interest. This is particularly the case when domain knowledge is inherently imprecise or vague. Concepts like that of a “near” destination (Berners-Lee and Hendler 2001), a “high Quality” audio system (McGuinness 2003), “many” children, a “faulty” reactor (Horrocks and Sattler 1999), “soon” and many more, require special modeling features. To bridge this gap fuzzy DLs have been introduced, which constitute an extension of classic DLs capable of representing and reasoning with vague and imprecise knowledge. Fuzzy DLs have already attracted the interest of researchers from other communities and have been used in numerous domains like multimedia and information retrieval applications (Meghini et al. 2001; Simou et al. 2008; Dasiopoulou et al. 2008) to provide ranking degrees, ontology alignment (Ferrara et al. 2008), matchmaking (Ragone et al. 2009) and many more.

Over the recent years, many expressive fuzzy DL languages have been studied, like fuzzy $\mathcal{SHIN}$ (Stoilos et al. 2007), fuzzy $\mathcal{ALCF}(D)$ (Straccia and Bobillo 2007) and fuzzy $\mathcal{SROIQ}$ (Bobillo et al. 2007), while implementation efforts of the introduced algorithms resulted in systems like FiRE,¹ fuzzyDL ² and DELOREAN.³ The previously mentioned systems are based on fuzzy extensions of worst-case exponential algorithms and although optimizations for them have also been studied recently (Simou et al. 2010; Haarslev et al. 2007), their scalability is still questionable as no evidence of any large-scale experimental evaluation has been presented. As a consequence, like in the case of classical DLs, much interest has emerged about the development of sound and complete inference algorithms for tractable, i.e. of at most polynomial complexity, fragments of fuzzy DLs.

To meet this objective, various approaches based on different classic DL systems have been proposed. Straccia (2006) introduced a fuzzy extension of the DL-Lite (Calvanese et al. 2007b) language, while Pan et al. (2007) presented the very first scalable system based on fuzzy-DL-Lite which is able to answer expressive fuzzy conjunctive queries over millions of data. On the other hand several works have also been conducted around the $\mathcal{EL}$ family of DLs (Baader et al. 2005). First Vojtáš presented a fuzzy extension of $\mathcal{EL}$ (Vojtáš 2007) while Stoilos et al. (2008) examined a fuzzy extension of the tractable language $\mathcal{EL}^{+}$.

The fuzzy $\mathcal{EL}^{+}$ DL presented in Stoilos et al. (2008) has many interesting properties since it extends concept axioms with degrees of truth, thus allowing for fuzzy concept inclusion. Nevertheless, the proposed language provides a sound and complete algorithm only for the problem of fuzzy concept subsumption, which makes it inappropriate for representing assertional knowledge. In other words, fuzzy ${\mathcal{EL}}^+$ can only be used for classification purposes since reasoning on knowledge bases that share individuals, which is the case in most real life applications, is not supported. Furthermore, it lacks the ability to reason with datatype properties that are widely used in real life applications. By using them one can model statements like “Paul is 180 cm height” or “John smokes more than 15 cigarettes per day”. In Example 1 we illustrate the expressive power of fuzzy ${\mathcal{EL}^{++}}$ using a medical application scenario.

Example 1

In the context of the ASSIST project ⁴ an ontology about cervical cancer is constructed (Mitkas et al. 2008; Falelakis et al. 2009). The diagnosis of cervical cancer is based mainly on three types of examination, namely cytology, colposcopy, and histology. Each patient may have one or more of these examinations that have one of the results presented in Table 1. According to the findings of the examinations each woman is characterized by some severity index. Each woman with a severity index 0 is considered healthy while each woman with a severity index 3 has invasive cervical cancer.

$$ \begin{array}[t]{l} \exists hasCytologyResult.ASSIST0CytologyResult\sqsubseteq\\ \ \ \ \ \ \ \ \ \ \ \ \ \ \exists hasSeverityIndex.ASSIST0SeverityIndex \end{array} $$

Table 1 Cytology, colposcopy and histology classification

Unfortunately the crisp ${\mathcal{EL}^{++}}$ language does not allow to express the fact that the findings of a histology examination are more important than those of a cytology examination. This can be achieved if we adopt a fuzzy version of ${\mathcal{EL}^{++}}$ to provide ranking degrees w.r.t. the confidence about the results of each examination—similar approaches have been proposed for multimedia retrieval, information retrieval, and ontology alignment applications (Meghini et al. 2001; Simou et al. 2008; Dasiopoulou et al. 2008; Ferrara et al. 2008). For example the following fuzzy concept inclusions

$$ \begin{array}[t]{l} \langle \exists hasCytologyResult.ASSIST0CytologyResult\sqsubseteq\\ \ \ \ \ \ \ \ \ \ \ \ \ \ \exists hasSeverityIndex.ASSIST0SeverityIndex,0.6\rangle \\ \langle \exists hasHistologyResult.ASSIST0HistologyResult\sqsubseteq\\ \ \ \ \ \ \ \ \ \ \ \ \ \ \exists hasSeverityIndex.ASSIST0SeverityIndex,0.8\rangle \end{array} $$

can be used to express the fact that the histology examination is more important, regarding the diagnosis about the severity index results, than the Cytology examination. Another advantage in using ${\mathcal{EL}^{++}}$, instead of fuzzy ${\mathcal{EL}^{+}}$, to represent our knowledge, is that it also provides for nominals and concrete domains. Nominals allow to relate our terminological knowledge to some assertional knowledge, i.e. information concerning different patients. For example we can assert that patient137 has a cytology examination with an ASSIST0 result:

$$ \begin{array}[t]{l} (\exists hasCytologyResult.ASSIST0CytologyResult)(patient137)\geq1 \end{array} $$

On the other hand concrete domains allow to represent numerical information about patients. For example the assertion

$$ \succcurlyeq_{15}(smokesCigarettesPerDay)(patient137)\geq 1 $$

indicates that patient137 smokes more than 15 cigarettes per day.

Motivated by the above scenario, in this paper we study a fuzzy extension of the $\mathcal{EL}^{++}$ language. Similar to fuzzy $\mathcal{EL}^{+}$, fuzzy $\mathcal{EL}^{++}$ allows for concept inclusion axioms extended with degrees of truth (Straccia 2005b). Additionally though, it allows for nominals, the bottom concept, and fuzzy concrete domains which add extra expressiveness. The main contributions of this paper can be summarized as follows:

• It presents the syntax and the semantics of fuzzy $\mathcal{EL}^{++}$ which is more expressive than fuzzy $\mathcal{EL}^{+}$ due to nominals, the bottom concept, and fuzzy concrete domains.

• It studies and presents the reduction of the most common inference services of fuzzy DL systems to the fuzzy concept subsumption problem. It is important to note at this point that such kind of reduction has not been studied in the fuzzy DL literature before.

• It investigates fuzzy p-admissible concrete domains for the fuzzy ${\mathcal{EL}^{++}}$ language—i.e. fuzzy concrete domains that can be integrated to the fuzzy ${\mathcal{EL}^{++}}$ language without affecting its polynomial time complexity.

• It presents a reasoning algorithm for the problem of fuzzy concept subsumption in fuzzy $\mathcal{EL}^{++}$ along with a detailed proof of its soundness and completeness.

• It investigates on the complexity of the algorithm.

The main objective of this paper is not to present a language that is more expressive than previously presented fuzzy DL languages “most of the expressive features appearing in this paper have already been presented in the literature”. It rather studies the interaction between expressiveness and complexity in order to introduce a fuzzy DL language that is expressive enough to be used in real world applications and at the same time retains its polynomial complexity reasoning algorithm.

The rest of the paper is organized as follows. Section 2 briefly introduces the DL ${\mathcal{EL}^{++}}$ and provides some preliminaries about the notion of a fuzzy set and how set theoretic and logical operations are extended to the fuzzy set framework. Section 3 introduces the syntax and semantics of the fuzzy ${\mathcal{EL}^{++}}$ language, presents the most common inference problems, and how these are reduced to the problem of fuzzy concept subsumption. Section 4 provides an investigation on the semantics of fuzzy concrete domains and on how they can be embedded into the fuzzy ${\mathcal{EL}^{++}}$ language. In Section 5 we present in detail the reasoning procedure for deciding fuzzy concept subsumption w.r.t. a fuzzy ${\mathcal{EL}^{++}}$ ontology and we provide the proofs for soundness, completeness, and the complexity of the proposed algorithm. Finally, in Section 6 we review related work on other fuzzy ${\mathcal{EL}}$ languages and fuzzy concrete domains, while Section 7 concludes the paper.

2 Preliminaries

2.1 The ${\mathcal{EL}^{++}}$ language

In the current section we briefly introduce the Description Logic ${\mathcal{EL}^{++}}$ which we will extend in the next sections.

The signature of ${\mathcal{EL}^{++}}$ (Baader et al. 2005) consists of disjoint sets of concept names (unary predicates) N _C , role names (binary predicates) N _R , and individuals (constants) N _I . ${\mathcal{EL}^{++}}$ concepts (or concept descriptions) are defined using the constructors presented in the upper part of Table 2 where a and b denote individuals, r,r ₁,...,r _k and s denote role names and C, D denote arbitrary concepts.

Table 2 Syntax and semantics of $\mathcal{EL}^{++}$

An ${\mathcal{EL}^{++}}$ ontology $\mathcal{O}$ is a pair $\langle{\mathcal{A}},\mathcal{C} \rangle$, where ${\mathcal{A}}$ is an assertional box (ABox) and ${\mathcal{C}}$ is a constraint box (CBox). An ${\mathcal{EL}^{++}}$ ABox is a finite set of concept and role assertions, while an ${\mathcal{EL}^{++}}$ CBox is a finite set of general concept inclusions (GCIs) and role inclusions (RIs). The syntaxes of both ABox and CBox are shown in Table 2.

The semantics of an ${\mathcal{EL}^{++}}$ ontology are given via an interpretation $\mathcal{I}=\langle \Delta^{\mathcal{I}},\cdot^{\mathcal{I}}\rangle$. The domain $\Delta^{\mathcal{I}}$ is a non-empty set of objects and the interpretation function $\cdot^{\mathcal{I}}$ maps each concept name A ∈ N _C to a subset $A^{\mathcal{I}}$ of $\Delta^{\mathcal{I}}$, each role name r ∈ N _R to a binary relation $r^{\mathcal{I}}$ on $\Delta^{\mathcal{I}}$, and each individual name a ∈ N _I to an element $a^{\mathcal{I}}\in\Delta^{\mathcal{I}}$. An interpretation $\mathcal{I}$ is a model of an ontology $\mathcal{O}=\langle {\mathcal{A}},\mathcal{C}\rangle$ if it is a model of ${\mathcal{A}}$ and ${\mathcal{C}}$. $\mathcal{I}$ is a model of an ABox ${\mathcal{A}}$ (CBox $\mathcal{C}$) iff every concept and role assertion in ${\mathcal{A}}$ (GCI and RI in $\mathcal{C}$) satisfy the semantics of ${\mathcal{EL}^{++}}$ concept descriptions shown in the third column of Table 2.

${\mathcal{EL}^{++}}$ with concrete domains

Numerical information is expressed in DLs with the aid of “concrete domains” (Baader et al. 2005). A concrete domain ${\mathcal{D}}$ is a pair $\langle \Delta^{{\mathcal{D}}},\mathcal{P}^{{\mathcal{D}}} \rangle$ with $\Delta^{{\mathcal{D}}}$ a set of concrete objects (values) and $\mathcal{P}^{{\mathcal{D}}}$ a set of predicate names, where each $p\in\mathcal{P}^{{\mathcal{D}}}$ is associated with an arity n > 0 and an extension $p^{\mathcal{D}}\subseteq (\Delta^{\mathcal{D}})^{n}$.

Example 2

The concrete domain of rational numbers $Q= \langle\mathbb{Q},\mathcal{P}^{Q} \rangle$, presented in Baader et al. (2005), has as domain the rational numbers and contains unary predicates such as $\top_{Q}$, =  _q , >  _q and binary predicates such as =, +  _q (where q ∈ ℚ). Intuitively a conjunction of the form:

$$ (=_{3} ) (x )\wedge (+_{5} ) (x,y ) $$

indicates that x = 3 and that x + 5 = y. It is obvious that such a conjunction is satisfiable and also the following holds:

$$ (=_{3} ) (x )\wedge (+_{5} ) (x,y )\models (=_{8} ) (y ). $$

To provide a link between ${\mathcal{EL}^{++}}$ and some arbitrary concrete domain, Baader et al. introduce a set of feature names N _F . The syntax and semantics of ${\mathcal{EL}^{++}}$ concrete domains are illustrated in Table 2, where p denotes a predicate of some concrete domain ${\mathcal{D}}_{j}$, f ₁,...,f _k are feature names, and an interpretation function $\cdot^{\mathcal{I}}$ maps each feature name f ∈ N _F to a partial function $f^{\mathcal{I}}$ from $\Delta^{\mathcal{I}}$ to $\Delta^{\mathcal{D}}$. For example using the ${\mathcal{EL}^{++}}$ syntax we may assert that “John is 30 years old” as follows: = ₃₀ (hasAge ) (John). The DL ${\mathcal{EL}^{++}}$ may be equipped with a number of concrete domains ${\mathcal{D}}_{1},\ldots,{\mathcal{D}}_{n}$ such that $\Delta^{{\mathcal{D}}_{i}}\cap\Delta^{{\mathcal{D}}_{j}}=\emptyset$ for i ≠ j.

2.2 Fuzzy sets

In this section we briefly introduce fuzzy set theory and fuzzy logic (Klir and Yuan 1995).

Let Ω be a (possibly infinite) set of elements. Any classical (crisp) subset S of Ω can be defined with the aid of a characteristic function χ _S :Ω→{0,1}, such that χ _S (x) = 1 if x ∈ S, and χ _S (x) = 0 otherwise. On the other hand, a fuzzy subset A of Ω is defined using a (so-called) membership function μ _A :Ω→[0,1] denoting that x belongs to A to a certain degree. Similarly, an n-ary fuzzy relation R over the sets Ω ₁,...,Ω _n is defined by a mapping μ _R :Ω ₁×...×Ω _n →[0,1]. For instance, TallHuman(John) = 0.8 implies that John belongs to the (fuzzy) set TallHumans to a degree of 0.8, i.e. that he is quite tall. Similarly, hasFriend (John,Mary ) = 0.9 states that Mary is a close friend of John.

2.2.1 Fuzzy set theoretic operations

The classical set theoretical and logical operations (complement, union, and so on) are extended in fuzzy set theory by using special mathematical functions (Klir and Yuan 1995). More precisely fuzzy complement, fuzzy intersection, fuzzy union, and fuzzy implication correspond (respectively) to an unary operation of the form c: [0,1 ]→[0,1], a binary operation of the form i: [0,1 ]×[0,1 ]→[0,1] (called t-norm), a binary operation of the form u: [0,1 ]×[0,1 ]→[0,1] (called t-conorm), and a binary operation $\mathcal{J}: [0,1 ]\times [0,1 ]\rightarrow [0,1]$.

In order to produce meaningful results, these functions must satisfy certain mathematical properties. For example, fuzzy complement must satisfy the following axiomatic requirements c (0 ) = 1, c (1 ) = 0, and c must be a monotonically decreasing function. The reader is referred to Klir and Yuan (1995) for a comprehensive introduction to fuzzy set theoretic operations. In Table 3 some popular families of fuzzy operators are presented.

Table 3 Popular families of fuzzy operators

Finally, given two binary fuzzy relations R ₁:Ω ₁×Ω ₂→[0,1 ] and R ₂: Ω ₂×Ω ₃→[0,1 ], their sup-t composition is defined as follows:

$$ \big[R_{1}\circ^{i}R_{2} \big] (a,c )=\sup_{b\in\Omega_{2}} \big\{ i (R_{1} (a,b ),R_{2} (b,c ) ) \big\} $$

where i is a t-norm. Due to the associativity property of sup-t composition, i.e. $(R_{1}\circ^{i}R_{2})\circ^{i}R_{3}=R_{1}\circ^{i} (R_{2}\circ^{i}R_{3} )$, we can extend the operation to any number of fuzzy relations, i.e. $[R_{1}\circ^{i}R_{2}\circ^{i}\ldots\circ^{i}R_{n} ] (a,b )$.

3 The fuzzy $\boldsymbol{\mathcal{EL}^{++}}$ language

3.1 Syntax and semantics

In this section we present the syntax and semantics of a fuzzy extension of the $\mathcal{EL}^{++}$ language. Since the semantics we propose are based on the operators of the Gödel logic, we may as well call the proposed language $\textnormal{f}_{G}$-$\mathcal{EL}^{++}$. Our extension follows in principle the syntax and semantics of fuzzy DLs previously presented in Straccia (2001) and Stoilos et al. (2007).

Like classical (crisp) ${\mathcal{EL}^{++}}$, the language of $\textnormal{f}_{G}$-$\mathcal{EL}^{++}$ consists of concept names N _C , role names N _R and individuals N _I . As usual individuals represent the objects of our universe, concept names represent fuzzy sets of individuals, and role names represent binary fuzzy relations between individuals of our universe.

The abstract syntax of concepts and roles is the same as their ${\mathcal{EL}^{++}}$ counterparts; however their semantics is based on fuzzy interpretations. A fuzzy interpretation $\mathcal{I}=\langle \Delta^{\mathcal{I}},\cdot^{\mathcal{I}}\rangle$ consists of a domain $\Delta^{\mathcal{I}}$ which is a non-empty set of objects and a fuzzy interpretation function $\cdot^{\mathcal{I}}$ which maps: (i) each a ∈ N _I to an element $a^{\mathcal{I}}\in\Delta^{\mathcal{I}}$, (ii) each A ∈ N _C to a membership function $A^{\mathcal{I}}:\Delta^{\mathcal{I}}\rightarrow[0,1]$, (iii) each r ∈ N _R to a membership function $r^{\mathcal{I}}:\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}\rightarrow[0,1]$. For example, for some interpretation $\mathcal{I}$, if $x\in\Delta^{\mathcal{I}}$ then $A^{\mathcal{I}}(x)$ gives the degree that the object x belongs to the fuzzy concept A, e.g. $A^{\mathcal{I}}(x)=0.8$.

Fuzzy $\mathcal{EL}^{++}$ allows to inductively define complex concept descriptions using the same constructors as the classic ${\mathcal{EL}^{++}}$ language. As with classical ${\mathcal{EL}^{++}}$ the semantics of concept descriptions are inductively defined. They are presented in the upper part of Table 4 for each $x\in\Delta^{\mathcal{I}}$. They are based on the Gödel fuzzy theoretic operation functions defined in Section 2.2. For example, since the min function is used for conjunction, we have that $(C\sqcap D)^{\mathcal{I}}(x)=\min(C^{\mathcal{I}}(x),D^{\mathcal{I}}(x))$. We chose to interpret nominals in a standard way, i.e. { a} is interpreted as the singleton crisp set that contains exactly the object $a^\mathcal{I}$, thus $\{a\}^\mathcal{I}(x)=1$ if $x=a^\mathcal{I}$, 0 otherwise. For different choices the reader is referred to Bobillo et al. (2006).

Table 4 Syntax and semantics of fuzzy $\mathcal{EL}^{++}$

The terminological knowledge of a fuzzy ${\mathcal{EL}^{++}}$ ontology is expressed by a set of fuzzy general concept inclusions (fuzzy GCIs) and role inclusion axioms (RIs), called a constraint box (CBox) ${\mathcal{C}}$ (Baader et al. 2005). A fuzzy GCI is an axiom of the form $\langle C\sqsubseteq D,d\rangle$, where d ∈ (0,1] and C,D are concept descriptions (see also Straccia 2005b). A role inclusion axiom is an axiom of the form $r_{1}\circ\ldots\circ r_{k}\sqsubseteq s$, where r ₁,...,r _k ,s ∈ N _R .

The semantics of fuzzy GCIs and RIs are given in the middle part of Table 4 where $x,y\in\Delta^{\mathcal{I}}$ and the operator ∘  ^min corresponds to the sup- min composition described in Section 2.2. An interpretation $\mathcal{I}$ is a model of a CBox ${\mathcal{C}}$ iff, for each GCI and RI in ${\mathcal{C}}$, the conditions described in the middle part of Table 4 are satisfied. For example, let the CBox $\mathcal{C}=\{ \langle A\sqcap B\sqsubseteq D,0.7\rangle ,r_{1}\circ r_{2}\sqsubseteq s\}$, and let the interpretation $\mathcal{I}$ such that $\Delta^{\mathcal{I}}=\{ x,y,z\}$, $A^{\mathcal{I}}(x)=0.3$, $B^{\mathcal{I}}(x)=0.2$, $D^{\mathcal{I}}(x)=0.5$, $r_{1}^{\mathcal{I}}(x,y)=0.4$, $r_{2}^{\mathcal{I}}(y,z)=0.3$ and $s^{\mathcal{I}}(x,z)=0.3$. It can be easily verified that $\mathcal{I}$ satisfies our CBox.

Fuzzy $\mathcal{EL}^{++}$ also allows for an assertional box (ABox) $\mathcal{A}$, i.e. a finite set of concept and role assertions that are used to describe a snapshot of our world. The syntax and semantics of concept and role assertions are described in the bottom part of Table 4, where a,b ∈ N _I , C ∈ N _C , r ∈ N _R and d ∈ [0,1]. Using such expressive means we can say, for example, that Tall(John) ≥ 0.8 and friend(John,Mairy) ≥ 0.5, while an interpretation $\mathcal{I}$ that satisfies both assertions is the following: $\Delta^{\mathcal{I}}=\{ x,y\}$, $J{\kern-1pt}ohn^{\mathcal{I}}=x$, $Mairy^{\mathcal{I}}=y$, $Tall^{\mathcal{I}}(x)=0.9$, $friend^{\mathcal{I}}(x,y)=0.7$.

We point out that the language studied in Stoilos et al. (2008) is not able to capture such assertional knowledge due to the absence of nominals.

Finally, we say that an interpretation $\mathcal{I}$ is a model of a fuzzy ontology $\mathcal{O}=\langle \mathcal{A},\mathcal{C}\rangle$ iff it is, at the same time, a model of $\mathcal{A}$ and $\mathcal{C}$.

Example 3

Providing a detailed version of the ontology presented in Example 1 we have that:⁵

$$ \begin{array}{ccl} C & = & \{ \vphantom{x^{2}}\langle \exists hasCytologyResult.ASSIST0CytologyResult\sqsubseteq\\ & & \hfill\exists hasSeverityIndex.ASSIST0SeverityIndex,0.6\rangle ,\\ \par & & \langle \exists hasColposcopyResult.ASSIST0ColposcopyResult\sqsubseteq\\ & & \hfill\exists hasSeverityIndex.ASSIST0SeverityIndex,0.7\rangle ,\\ & & \langle \exists hasHistologyResult.ASSIST0HistologyResult\sqsubseteq\\ & & \hfill\exists hasSeverityIndex.ASSIST0SeverityIndex,0.8\rangle \ldots\vphantom{x^{2}}\} \\ {\mathcal{A}} & = & \{ \begin{array}[t]{l} (\exists hasCytologyResult.ASSIST0CytologyResult)(patient137)\geq1\end{array},\\ & & \ \begin{array}[t]{l} (\exists hasHistologyResult.ASSIST0HistologyResult)(patient138)\geq1\end{array}\} \end{array} $$

The first fuzzy GCI implies that if a patient has a cytology result of type ASSIST0 then this patient also has an ASSIST0 severity index with a degree of at least 0.6 (i.e. this patient participates with a degree of at least 0.6 in concept $\exists hasSeverityIndex.ASSIST0SeverityIndex$). In a similar manner, the other two GCIs state that the colposcopy and histology examination results imply degrees 0.7 and 0.8 respectively. Hence patient137 has an ASSIST0 severity index with a degree of at least 0.6 because of her cytology result, while patient138 belongs to the same concept with a degree of at least 0.8 because of her histology result.

In the specific scenario one can say that the degrees can be subsequently interpreted as degrees of confidence by the medical personnel. More specifically the concept

$$ \exists hasSeverityIndex.ASSIST0SeverityIndex $$

provides a ranking between the individuals participating in it. The higher the degree of participation an individual has on this concept, the higher is the confidence that this individual is healthy. Therefore since our ontology implies that

$$\begin{array}{rll} \mathcal{O} &\models& (\exists hasSeverityIndex.ASSIST0SeverityIndex)(patient137)\geq 0.6\\ \mathcal{O} &\models& (\exists hasSeverityIndex.ASSIST0SeverityIndex)(patient138)\geq 0.8 \end{array}$$

the medical personnel has a 0.6 confidence degree that patient137 is healthy and a 0.8 confidence degree that patient138 is healthy.

Other applications that adopt fuzzy DLs in order to provide ranking degrees have been proposed for multimedia, information retrieval, and ontology alignment applications (Meghini et al. 2001; Simou et al. 2008; Dasiopoulou et al. 2008; Ferrara et al. 2008).

The presence of nominals makes fuzzy ${\mathcal{EL}^{++}}$ much more expressive than fuzzy ${\mathcal{EL}^{+}}$ since it allows the representation of assertional knowledge for a large ontology containing patients or any other kind of information. Furthermore nominals along with the bottom concept allow to express the unique name assumption, i.e. that two individuals cannot correspond to the same object in $\Delta^{\mathcal{I}}$, as follows: ${\langle \{ a\} \sqcap \{ b\}\sqsubseteq{\bot},1\rangle}$. Finally, the bottom concept also allows to express disjointness between complex concept descriptions as follows: ${\langle C\sqcap D\sqsubseteq{\bot},1\rangle}$.

3.2 Fuzzy DL inference problems

In this section we present the most common inference problems addressed by fuzzy DLs and prove how each one can be reduced to the fuzzy concept subsumption problem.

Let $\mathcal{C}$ be a fuzzy ${\mathcal{EL}^{++}}$ CBox, ${\mathcal{A}}$ a fuzzy ${\mathcal{EL}^{++}}$ ABox, and $\mathcal{O}$ a fuzzy ${\mathcal{EL}^{++}}$ ontology. The most common inference problems addressed by fuzzy DL systems are the following:

Concept satisfiability :

A concept C is satisfiable w.r.t. $\mathcal{C}$, iff there exists a model $\mathcal{I}$ of $\mathcal{C}$ such that $C^{\mathcal{I}}(x)>0$ for some $x\in\Delta^{\mathcal{I}}$.

Fuzzy concept subsumption :

A concept C is fuzzily subsumed by a concept D, to a degree of d ∈ (0,1], w.r.t. $\mathcal{C}$, written $\langle C\sqsubseteq_{\mathcal{C}}D,d\rangle$, iff for every model $\mathcal{I}$ of $\mathcal{C}$ and $x\in\Delta^{\mathcal{I}}$ it holds that $\min(C^{\mathcal{I}}(x),d)\leq D^{\mathcal{I}}(x)$. We often abuse notation and write $\langle C \sqsubseteq_{\mathcal{O}}D,d\rangle$ if the ABox of the ontology is empty. We also write $\mathcal{O}\models{\langle C\sqsubseteq D,d\rangle}$ as an equivalent form of $\langle C\sqsubseteq_{\mathcal{O}}D,d\rangle$.

Ontology consistency :

We say that $\mathcal{O}=\langle {\mathcal{A}},\mathcal{C}\rangle$ is consistent iff it has at least one model.

Instance problem :

An individual a ∈ N _I is an instance of a concept C with a degree greater or equal than d, w.r.t. an ontology $\mathcal{O}$, iff in each model $\mathcal{I}$ of $\mathcal{O}$ it holds that $C^{\mathcal{I}}(a^\mathcal{I})\geq d$.

Greatest lower bound problem :

The greatest lower bound (GLB) problem for a crisp concept assertion C(a) is to find the largest degree d such that $C^{\mathcal{I}}(a^\mathcal{I})\geq d$ holds for every model $\mathcal{I}$ of ${\mathcal{O}}$.

As the following Lemma suggests all inference problems can be reduced in linear time to the fuzzy concept subsumption problem:

Lemma 1

Let ${\mathcal{O}}=\langle {\mathcal{A}},\mathcal{C}\rangle$ be a fuzzy ${\mathcal{EL}^{++}}$ ontology, with ${\mathcal{A}}$ the fuzzy ${\mathcal{EL}^{++}}$ ABox and $\mathcal{C}$ the fuzzy CBox, and let C a fuzzy ${\mathcal{EL}^{++}}$ concept. All inference problems of fuzzy DLs can be reduced to fuzzy concept subsumption as follows:

• Concept satisfiability: concept C is satisfiable w.r.t. $\mathcal{C}$ iff $\langle C\not\sqsubseteq_{\mathcal{C}}\bot,1\rangle$.

• Instance problem: in order to solve the instance problem our algorithm replaces each assertion in ${\mathcal{A}}$ with a fuzzy GCI between a nominal and a concept. Henceforth, instance checking can be reduced to fuzzy concept subsumption between a nominal and a concept. Let the set $\mathcal{C_{A}}$ defined as follows:

  $$\begin{array}{rll} \mathcal{C_{A}} & := & \{ \langle \{ a\} \sqsubseteq C,d\rangle \mid C(a)\geq d\in\mathcal{A}\} \\ && \bigcup\, \{ \langle \{ a\} \sqsubseteq\exists r.\{ b\} ,d\rangle \mid r(a,b)\geq d\in\mathcal{A}\} . \end{array}$$

  An individual c is an instance of C , to a degree at least d , w.r.t. ${\mathcal{O}}$ , iff $\langle \{ c\} \sqsubseteq_{\mathcal{C}\cup\mathcal{C}_{{\mathcal{A}}}}C,d^{\prime}\rangle$ for some d′ ≥ d.

  We must point out that our algorithm when calculating concept subsumption between a nominal {c} and a concept D , it calculates the greatest degree d such that ${\mathcal{O}}\models{\langle \{c\}\sqsubseteq D,d\rangle}$ . Therefore simultaneously solves the GLB problem.

• Ontology consistency: ${\mathcal{O}}$ is consistent iff $\langle \top\not\sqsubseteq_{\mathcal{C}\cup\mathcal{C}_{{\mathcal{A}}}}\bot,1\rangle$ , where $\mathcal{C}_{{\mathcal{A}}}$ is as before.

Consequently, like in the case of crisp $\mathcal{EL}^{++}$, we will only focus in solving the fuzzy concept subsumption problem.

4 Extending fuzzy ${\mathcal{EL}^{++}}$ with fuzzy concrete domains

Fuzzy concrete domains allow us to represent and reason about “fuzzy concrete qualities”. The need for fuzzy arithmetic and subsequently fuzzy concrete domains emerges from a variety of applications (mechanical, geotechnical and biomedical engineering). For an extensive presentation of the theory of fuzzy arithmetic and an extensive view on its applications the reader may refer to Hanss (2005).

In the rest of this section (i) we revise the syntax and semantics of fuzzy concrete domains, initially introduced in Straccia (2005a), (ii) we introduce the notion of conjunction, disjunction, solution, and implication on a fuzzy concrete domain, (iii) we adapt the syntax and semantics of the concrete domain constructor introduced for the crisp ${\mathcal{EL}^{++}}$ language (Baader et al. 2005) for the fuzzy case, (iv) we introduce a set of restrictions on the expressiveness of fuzzy ${\mathcal{EL}^{++}}$ fuzzy concrete domains in order to ensure the language’s polynomial complexity.

4.1 Fuzzy concrete domains

Straccia (2005a) first studied fuzzy concrete domains in the fuzzy DL $\mathcal{ALC}({\mathcal{D}})$. According to Straccia, a fuzzy concrete domain $\mathcal{D}$ is a pair $\langle \Delta^{\mathcal{D}},\Phi^{\mathcal{D}}\rangle$ where $\Delta^{\mathcal{D}}$ is a set and $\Phi^{\mathcal{D}}$ is a set of fuzzy predicate names. Each fuzzy predicate $p\in\Phi^{\mathcal{D}}$ with a predefined arity n has an interpretation $p^{\mathcal{D}}:(\Delta^{\mathcal{D}})^{n}\rightarrow[0,1]$, which is an n-ary fuzzy relation over $\Delta^{\mathcal{D}}$.

For a concrete domain $\mathcal{D}$ a conjunction of m formulae with degrees has the following form:

$$\label{eq:formulae_conjuntion} \bigwedge_{i=1}^{m}p_{i}(\overline{X}_{i})\bowtie_{i}d_{i} $$

(1)

where $p_{i}\in\Phi^{\mathcal{D}}$ is a concrete domain predicate, $\overline{X}_{i}$ is a vector of variable names with the same arity as p _i , ⋈  _i  ∈ { ≤ , < , = , > , ≥ } , d _i  ∈ (0,1], and 1 ≤ i ≤ m.

We say that (1) is satisfiable, iff there exists a mapping δ from variable names to the elements of our concrete domain $\delta:\left(\bigcup_{i=1}^{m}\overline{X}_{i}\right)\rightarrow\Delta^{\mathcal{D}}$, such that $\mbox{\ensuremath{p_{i}^{\mathcal{D}_{j}}(\delta(\overline{X}_{i}))\bowtie_{i}d_{i}}}$ holds⁶ for every formula in the conjunction. We call the mapping δ a solution for the conjunction, denoted as $\delta\models\bigwedge_{i=1}^{m}p_{i}(\overline{X}_{i})\bowtie_{i}d_{i}.$ In any different case we say that the conjunction is unsatisfiable. A conjunction of fuzzy concrete domain predicates implies a disjunction of fuzzy concrete domain predicates i.e.

$$ \bigwedge_{i=1}^{m}p_{i}(\overline{X}_{i})\bowtie_{i}d_{i} \models\bigvee_{i=m+1}^{n}p_{i}(\overline{X}_{i})\bowtie_{i}d_{i} $$

iff for every solution δ of the conjunction we have that $\mbox{\ensuremath{\delta\models p_{l}((\overline{X}_{l}))\bowtie_{l}d_{l}}}$ for some m + 1 ≤ l ≤ n.

Example 4

The concrete domain $\mathcal{F}^{\prime\prime}=\langle \mathbb{Q},\Phi^{\mathcal{F}^{\prime\prime}}\rangle$ defined on the set of rational numbers contains the unary predicate $\succcurlyeq_{q}$ and the binary predicate ${ \succcurlyeq _{ + q}}$ for every q ∈ ℚ. The two predicates can be defined based on some monotonic, continuous, increasing function such as the following:

$$ \begin{array}{c} f_q(x)= \begin{cases} 0 \quad ,\ x<q-10\\ \dfrac{x-q+10}{10} & ,\ q-10\leq x\leq q\\ 1 & ,\ q<x \end{cases} \end{array}. $$

Based on the previous membership functions the two predicates are interpreted as follows: $\succcurlyeq _q^\mathcal{D}(x) = {f_q}(x)$ and $\succcurlyeq _{ + q}^\mathcal{D}(x,y) = {f_q}(x - y)$

The formula ${ \succcurlyeq _{ + q}}\left( x \right)$ is used to indicate that the variable x is fuzzily superior to the value of q, while the formula ${ \succcurlyeq _{ + q}}\left( {x,y} \right)$ is used to indicate that the variable x is fuzzily superior to the addition of the variable y and the value of q. The membership function f ₂₀, illustrated in Fig. 1, gives a value of 0 to every x ∈ ℚ lesser than 10, a value of 1 to every x ∈ ℚ greater than 20, and a value in-between to every other x ∈ ℚ. Therefore an assertion of the form $\succcurlyeq_{20}(x)\geq 1$ (respectively ${ \succcurlyeq _{ + 20}}\left( {x,y} \right)$) indicates that δ(x) ≥ 20 (respectively δ(x) ≥ 20 + δ(y)) for every solution δ of the previous assertion.

Fig. 1

The $\succcurlyeq_{15}$ and the $\succcurlyeq_{20}$ membership functionsFigures 1–3 -EPS vs PDF differs in background. Please check.

4.2 Fuzzy ${\mathcal{EL}^{++}}$ with concrete domains

Knowledge related to some fuzzy concrete domain is embodied into a fuzzy ${\mathcal{EL}}^{++}$ ontology via the fuzzy concrete domain constructor. As it can be seen in Table 5, the fuzzy concrete domain constructor we propose has the same syntax as its crisp counterpart presented in Baader et al. (2005). As a result, in order to provide a link between the DL and some fuzzy concrete domain, a set N _F of feature names is introduced. The concept description p(f ₁,...,f _k ) presented in Table 5 is constructed by a predicate of some concrete domain ${\mathcal{D}}$ and the feature names f ₁,...,f _k . Intuitively the predicate p, along with some degree d ∈ [0,1] dictates the relation between the features f ₁,...,f _n .

Table 5 Syntax and semantics of the concrete domain constructor for fuzzy $\mathcal{EL}^{++}$

Example 5

Suppose that we have the predicate $\succcurlyeq_{20}$ defined in Example 4 and the feature name $\textnormal{smokesCigarettesPerDay}$. A concept inclusion of the form

$$ \langle{\succcurlyeq_{20}(\textnormal{smokesCigarettesPerDay})}\sqsubseteq{\textnormal{HeavySmoker}},1\rangle $$

indicates that someone that smokes more than 20 cigarettes per day is a heavy smoker. Likewise a concept assertion of the form

$$ \succcurlyeq_{15}(\textnormal{smokesCigarettesPerDay})(J{\kern-1pt}ohn)\geq1 $$

states that John smokes more than 15 cigarettes per day.

As usual, the DL fuzzy $\mathcal{EL}^{++}$ may be equipped with a number of concrete domains $\mathcal{D}_{1},\ldots,\mathcal{D}_{n}$ such that $\Delta^{\mathcal{D}_{i}}\cap\Delta^{\mathcal{D}_{j}}=\emptyset$ for 1 ≤ i < j ≤ n. If we want to stress out the use of particular concrete domains $\mathcal{D}_{1},\ldots,\mathcal{D}_{n}$, we write fuzzy $\mathcal{EL}^{++}(\mathcal{D}_{1},\ldots,\mathcal{D}_{n})$ instead of fuzzy $\mathcal{EL}^{++}$.

In order to handle feature names, an interpretation $\mathcal{I}$ is extended by mapping each feature name f ∈ N _F to a partial function $f^{\mathcal{I}}:\Delta^{\mathcal{I}}\rightarrow\bigcup_{1\leq i\leq n}\Delta^{{\mathcal{D}}_{i}}.$ The extension of $\cdot^{\mathcal{I}}$ in order to interpret the concrete domain concept description is presented in Table 5.

Example 6

A possible interpretation for Example 5 is the following: $\Delta^{\mathcal{I}} =\{ J{\kern-1pt}ohn^{\mathcal{I}}\}$, $\textnormal{smokesCigarettesPerDay}^{\mathcal{I}}(J{\kern-1pt}ohn^{\mathcal{I}}) =15$, $\textnormal{HeavySmoker}^{\mathcal{I}}(V^{\mathcal{I}}) =0.5$. The previous interpretation is a model since:

$$\begin{array}{rll} (\succcurlyeq_{15}(\textnormal{smokesCigarettesPerDay}))^{\mathcal{I}}(J{\kern-1pt}ohn^{\mathcal{I}}) & = & 1\\ (\succcurlyeq_{20}(\textnormal{smokesCigarettesPerDay}))^{\mathcal{I}}(J{\kern-1pt}ohn^{\mathcal{I}}) & = & 0.5 \end{array}$$

and therefore the ABox and the CBox are satisfied.

Unfortunately, unrestricted use of fuzzy concrete domains may lead to some non polynomial or even undecidable language. For example, it is obvious that the language fuzzy ${\mathcal{EL}^{++}}({\mathcal{D}})$, where ${\mathcal{D}}$ is some language of exponential complexity, is a language of at least exponential complexity. Even worse, as shown in Lutz (2003), combining decidable description logics and decidable concrete domains may even lead to undecidable languages.

In order to ensure that our language is of polynomial complexity, we must impose a set of restrictions on the expressiveness of the concrete domain. These restrictions, that are an adaptation for the fuzzy case of those presented in Baader et al. (2005), result in two different categories of fuzzy p-admissible concrete domains: loose fuzzy p-admissible concrete domains and strict fuzzy p-admissible concrete domains.

Loose fuzzy p-admissible concrete domains are more expressive than strict. Due to their expressiveness, their utilization must be limited in order to ensure a sound, complete, and polynomial algorithm. Therefore, a concept p(f ₁,...,f _k ) is only allowed in concept inclusions of the form:

$$\begin{array}{rll} & \langle \{ a\} \sqsubseteq p(f_{1},\ldots,f_{k}),d\rangle \label{eq:nominal-loose fuzzy p admissible concept}\end{array}$$

(2)

$$\begin{array}{rll} & \langle p(f_{1},\ldots,f_{k})\sqsubseteq C,d\rangle \label{eq:loose fuzzy p admissible concept - Concept description} \end{array}$$

(3)

where { a} is some nominal in our ontology and C can be some arbitrary concept description as long as neither it, nor some of its subconcepts, is a concrete domain expression. On the other hand, strict fuzzy p-admissible concrete domain concepts may be used in any part of a concept inclusion since their limited expressiveness ensures that the fuzzy ${\mathcal{EL}^{++}}$ language will remain sound, complete, and terminating.

Definition 1

(Loose Fuzzy p-admissible Concrete Domain) A concrete domain $\mathcal{D}$ is loosely fuzzy p -admissible if it has the following properties:

• 1. Satisfiability and implication in $\mathcal{D}$ are decidable in polynomial time.

• 2. $\mathcal{D}$ is convex, i.e. if a conjunction of atoms of the form $p_{i}(\overline{X}_{i})\geq d_{i}$ implies a disjunction of such atoms, then it also implies one of its disjuncts.

The admissibility restrictions imposed on loose fuzzy p-admissible concrete domains are an immediate extension of the restrictions presented in Baader et al. (2005). The restriction of a polynomial time algorithm for deciding satisfiability and implication in ${\mathcal{D}}$ is obviously needed in order to ensure that the resulting language will be of polynomial complexity. The convexity restriction ensures that fuzzy concrete domains won’t introduce non-determinism to our language that ultimately would lead to a language of non polynomial complexity. The concrete domain presented in Example 4 without the presence of $\succcurlyeq$ _{+  q} predicates is loosely fuzzy p-admissible as proved in Proposition 1 in the Appendix.

Example 7

In this example we will present a fuzzy concrete domain that does not satisfy Condition 2 of Definition 1 and we will show how it can introduce non determinism to our language. 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 unary predicates ≃ _0.5, ≃ ₁ , ≃ _1.5 whose membership functions are depicted on Fig. 2.

Fig. 2

The ≃ _0.5, ≃ ₁, and ≃ _1.5 membership functions

Suppose now that we have a formula with degree of the form ≃ ₁(x) ≥ 0.5. The previous inequality along with the membership function of the ≃ ₁ predicate imply that every solution δ of the previous conjunction maps the variable name x to some element in [0.5,1.5]. With similar arguments we also have that each solution δ′ of ≃ _0.5(x) ≥ 0.5 maps x to some element in [0,1], while each solution δ′′ of ≃ _1.5(x) ≥ 0.5 maps x to some element in [1,2]. Therefore it can be verified that

$$ \simeq_1(x)\geq 0.5 \models \simeq_{0.5}(x)\geq 0.5\bigvee \simeq_{1.5}(x)\geq 0.5 $$

applies, while ≃ ₁(x) ≥ 0.5 ⊧ ≃ _0.5(x) ≥ 0.5 and ≃ ₁(x) ≥ 0.5 ⊧ ≃ _1.5(x) ≥ 0.5 don’t apply. Therefore the presented concrete domain is non-convex.

Suppose now that we have an ${\mathcal{EL}^{++}}$ ontology of the form

$$ {\mathcal{O}}=\left\{ \langle\{a\}\sqsubseteq\simeq_{1}(f),{0.5}\rangle, \langle\simeq_{0.5}(f)\sqsubseteq{C},{1}\rangle, \langle{\simeq_{1.5}(f)}\sqsubseteq{D},{1}\rangle, \right\} $$

where f is some feature name. According to the previous findings we can conclude that for every model $\mathcal{I}$ of ${\mathcal{O}}$ either $\mathcal{I}\models \langle{\{a\}}\sqsubseteq{C},{0.5}\rangle$ holds or $\mathcal{I}\models \langle{\{a\}}\sqsubseteq{D},{0.5}\rangle$ holds, while neither ${\mathcal{O}}\models \langle{\{a\}}\sqsubseteq{C},{0.5}\rangle$ nor ${\mathcal{O}}\models \langle{\{a\}}\sqsubseteq{D},{0.5}\rangle$ hold. Therefore the corresponding language is non-deterministic and consequently of non-polynomial complexity.

We proceed to define strictly fuzzy p-admissible concrete domains that are a more restrictive subset of loosely fuzzy p-admissible concrete domains.

Definition 2

(Strict Fuzzy p-admissible Concrete Domain) A concrete domain $\mathcal{D}$ is strictly fuzzy p -admissible, if it is loosely fuzzy p-admissible and has the following properties for some conjunction ${\textnormal{conj}}:=\bigwedge_{i=1}^{m}p_{i}(\overline{X}_{i}) \geq d_{i}$:

• 1. If the implications ${\textnormal{conj}}\models p(\overline{X})\geq d$, ${\textnormal{conj}} \not\models p(\overline{X})> d$ apply, then the implications ${\textnormal{conj}}^{\prime}\models p(\overline{X}) \geq \min(e,d)$, ${\textnormal{conj}}^{\prime}\not\models p(\overline{X}) > \min(e,d)$ will also apply for any degree e ∈ (0,1] and the conjunction

  $$ {\textnormal{conj}}^{\prime}:=\bigwedge_{i=1}^{m}p_{i}(\overline{X}_{i}) \geq \min(d_{i},e). $$

• 2. If the conjunction ${\textnormal{conj}}$ is unsatisfiable, then the conjunction ${\textnormal{conj}}^{\prime}$ is also unsatisfiable for every e ∈ (0,1].

• 3. If the implications ${\textnormal{conj}}\models p(\overline{X})\geq d$, ${\textnormal{conj}}\not\models p(\overline{X})>d$ apply, then d appears in the conjunction ${\textnormal{conj}}$.

• 4. If the implications ${\textnormal{conj}}\models p(\overline{X})\geq d$ and ${\textnormal{conj}} \not\models p(\overline{X})> d$ apply, then it also applies that ${\textnormal{conj}}^{\prime\prime}\models p(\overline{X})\geq d$, ${\textnormal{conj}}^{\prime\prime}\not\models p(\overline{X})> d$ for the conjunction:

  $$ {\textnormal{conj}}^{\prime\prime}:=\bigwedge_{p^{\prime}(\overline{X}^{\prime})\geq d^{\prime}\textnormal{ appears in }{\textnormal{conj}}\textnormal{ and } d^{\prime}\geq d} p^{\prime}(\overline{X^{\prime}})\geq d^{\prime}. $$

The previously mentioned admissibility restrictions were imposed by the proof process—they are used throughout the soundness, completeness, and complexity proofs—and thus it is difficult to give an intuitive explanation of each one of them. Nevertheless, the main intuition underlying these restrictions is that they prevent the production of new degrees. The production of new degrees along with the presence of fuzzy p-admissible concrete domain concepts in GCIs could lead our algorithm even to non termination. In Example 11 in the Appendix we show how the absence of these restrictions may alter the performance of our algorithm.

Having in mind the latest work of Baader and Peñaloza (2011) which proves that even inexpressive fuzzy DLs become undecidable with the addition of arbitrary t-norms in GCIs, it is interesting to investigate if the same applies with the presence of arbitrary concrete domains (even of polynomial complexity) since they both may introduce an arbitrary number of new degrees to an ontology ${\mathcal{O}}$.

We give an example of a fuzzy concrete domain that confines to the previously mentioned restrictions:

Example 8

We can formulate a fuzzy concrete domain $\mathcal{F}^{\prime}=\langle S\times[0,1],\Phi^{\mathcal{F}^{\prime}}\rangle$ where S is an arbitrary set of elements and $\Phi^{\mathcal{F}^{\prime}}$ contains a predicate =  _q for every q ∈ S. Therefore the interpretation of =  _q (i.e. $=_q^{\mathcal{D}}$) is a mapping $=_q^{\mathcal{D}}:S\times[0,1]\rightarrow [0,1]$ defined as follows for every element α ∈ S×[0,1]:

$$ =_q^{\mathcal{D}}(\alpha)= \begin{cases} d \quad \textnormal{ if } \alpha=\langle q, d\rangle \\ 0 \quad \textnormal{ otherwise}\\ \end{cases} $$

For example the conjunction

$$ =_5(x)\geq 0.3 \wedge =_5(x)\geq 0.5 \wedge =_8(y)\geq 0.6 . $$

has a solution δ such that $\delta(x)=\langle 5,0.5\rangle$, $\delta(y)=\langle 8,0.6\rangle$.

5 Reasoning in the fuzzy $\mathcal{EL}^{++}$ language

Since all reasoning problems of fuzzy $\mathcal{EL}^{++}$ can be reduced to fuzzy concept subsumption, it suffices to develop an algorithm for this problem only. The proposed algorithm, similar to that presented in Baader et al. (2005), is performed in two steps. Initially an ontology ${\mathcal{O}}$ is normalized and then an algorithm for deciding subsumption is applied over the normalized ontology.

5.1 Normal form of a fuzzy $\mathcal{EL}^{++}$ ontology

Given an ontology ${\mathcal{O}}$, the set of basic concept descriptions of ${\mathcal{O}}$, denoted as $BC_{{\mathcal{O}}}$, is the smallest set of concept descriptions that contains the top concept $\top$, all concept names and nominals in ${\mathcal{O}}$, and all subconcepts of the form p(f ₁,...,f _k ) appearing in ${\mathcal{O}}$. Similarly, $R_{{\mathcal{O}}}$ denotes the set of all role names in ${\mathcal{O}}$, and the set $[0,1]_{{\mathcal{O}}}$ is the subset of [0,1 ] containing only the degrees appearing in ${\mathcal{O}}$, i.e. $[0,1 ]_{{\mathcal{O}}}=\{ d\mid d\in [0,1 ]\textnormal{ and }\langle C\sqsubseteq D,d\rangle \in{\mathcal{O}}\}$. Since our algorithm focuses on the fuzzy concept subsumption problem and therefore works on an empty ABox according to Lemma 1, we won’t consider the ABox ${\mathcal{A}}$ for degrees.

A fuzzy $\mathcal{EL}^{++}$ ontology ${\mathcal{O}}$ is in normal form, iff all fuzzy GCIs in ${\mathcal{O}}$ are in one of the following forms (where $C_{1},C_{2}\in BC_{{\mathcal{O}}}$, $D\in BC_{{\mathcal{O}}}\cup\{ \bot\}$ and d ∈ (0,1]):

$$ \langle C_{1}\sqsubseteq D,d\rangle \ \ \ \ \ \langle C_{1}\sqsubseteq\exists r.C_{2},d\rangle \ \ \ \ \ \langle C_{1}\sqcap C_{2}\sqsubseteq D,d\rangle \ \ \ \ \ \langle \exists r.C_{1}\sqsubseteq C_{2},d\rangle $$

and all RIs are in either the form $r_{1}\sqsubseteq s$, or $r_{1}\circ r_{2}\sqsubseteq s$, for $r_{1},r_{2},s\in R_{{\mathcal{O}}}$.

As in the case with classical $\mathcal{EL}^{++}$ (Baader et al. 2005), a fuzzy $\mathcal{EL}^{++}$ ontology ${\mathcal{O}}$ can be normalised by exhaustively applying the rules of Table 6 where $\hat{C},\hat{D}\not\in BC_{{\mathcal{O}}}$ are concept descriptions, u denotes a new role name, and A a new concept name.

Table 6 Normalization rules for fuzzy $\mathcal{EL}^{++}$

Example 9

For example suppose that our ontology ${\mathcal{O}}$ contains only a GCI of the form $\langle{\exists r. (A\sqcap B)}\sqsubseteq{C \sqcap D},{0.3}\rangle$.

• Application of rule NF3 replaces the initial GCI with two GCIs of the form: $\langle{A\sqcap B}\sqsubseteq{E_1},{1}\rangle$ and $\langle{ \exists r. E_1}\sqsubseteq{C \sqcap D},{0.3}\rangle$ where E ₁ is a new concept name.

• Application of rule NF5 replaces the GCI $\langle{ \exists r. E_1}\sqsubseteq{C \sqcap D},{0.3}\rangle$ with two GCIs of the form $\langle{\exists r. E_1}\sqsubseteq{E_2},{1}\rangle$ and $\langle{E_2}\sqsubseteq{C\sqcap D},{0.3}\rangle$ where E ₂ is a new concept name.

• Application of rule NF7 replaces the GCI $\langle{E_2}\sqsubseteq{C\sqcap D},{0.3}\rangle$ with two GCIs of the form $\langle{E_2}\sqsubseteq{C},{0.3}\rangle$ and $\langle{E_2}\sqsubseteq{ D},{0.3}\rangle$.

Therefore the initial CBox $\mathcal{C}=\{ \langle{ \exists r. (A\sqcap B)}\sqsubseteq{C \sqcap D},{0.3}\rangle \}$ is transformed to the normalized CBox

$$ \mathcal{C}^{\prime}=\{ \langle{A\sqcap B}\sqsubseteq{E_1},{1}\rangle, \langle{\exists r. E_1}\sqsubseteq{E_2},{1}\rangle, \langle{E_2}\sqsubseteq{C},{0.3}\rangle, \langle{E_2}\sqsubseteq{ D},{0.3}\rangle. \} $$

where E ₁, E ₂ are newly introduced concept names.

Lemma 2

Fuzzy subsumption w.r.t. a fuzzy $\mathcal{EL}^{++}$ ontology ${\mathcal{O}}$ can be reduced in linear time to fuzzy subsumption w.r.t. a normalized fuzzy $\mathcal{EL}^{++}$ ontology ${\mathcal{O}}^{\prime}$.

5.2 A subsumption algorithm for fuzzy $\mathcal{EL}^{++}$

In this section we present the algorithm for deciding fuzzy concept subsumption w.r.t. to a normalized ontology ${\mathcal{O}}$. Initially we reduce the problem of fuzzy concept subsumption between two concept descriptions C and D to fuzzy concept subsumption between a newly introduced nominal and a newly introduced concept name.

Lemma 3

Let ${\mathcal{O}}$ be a fuzzy ${\mathcal{EL}^{++}}$ ontology and C and D fuzzy ${\mathcal{EL}^{++}}$ concepts. Then $\langle C\sqsubseteq_{{\mathcal{O}}}D,d\rangle$ , iff $\langle \{ o\} \sqsubseteq_{{\mathcal{O}}^{\prime}}B,d\rangle$ , where o is a new individual name, B a new concept name not appearing in $BC_{{\mathcal{O}}}$ and

$$ {\mathcal{O}}^{\prime}={\mathcal{O}}\cup\{ \langle{\{ o\}}\sqsubseteq C,1\rangle,\langle D\sqsubseteq B, 1\rangle\}. $$

Our reasoning algorithm works by saturating the input axioms using the rules in Table 7. The rules are applied over a normalized ontology ${\mathcal{O}}$ and produce new axioms of the form $\langle C\sqsubseteq D, d\rangle$, $\langle C\sqsubseteq \exists{r}.D,d\rangle$ where $r\in R_{\mathcal{O}}$ and $C,D\in BC_{\mathcal{O}}$. These new axioms are added to the saturated ontology ${{\mathcal{O}}_{\rm SAT}}$ which contains, explicitly, fuzzy concept subsumptions implied in ${\mathcal{O}}$. This means that if $\langle C\sqsubseteq D, d\rangle\in{{\mathcal{O}}_{\rm SAT}}$ then $\langle C\sqsubseteq_{{\mathcal{O}}}D,d\rangle$. The rules in Table 7 have the form

$$ \dfrac{U_{1},\ldots,U_{n}}{W}:V $$

where U ₁,...,U _n are concept inclusions in ${{\mathcal{O}}_{\rm SAT}}$, W is the concept inclusion that will be added in each rule application to ${{\mathcal{O}}_{\rm SAT}}$, and V is either a concept/role inclusion in ${\mathcal{O}}$, or a fuzzy concrete domain condition. The notation adopted by our algorithm is similar to the one presented in Kazakov (2009), rather than the one in Baader et al. (2005) and Stoilos et al. (2008).

Table 7 Saturation Rules for Fuzzy $\mathcal{EL}^{++}$ Ontologies

The saturation rules are performed in the following sequence. Initially rules I1, I2 are applied and then the algorithm proceeds with the application of the other completion rules described in Table 7 until no rule can add any further information. By the semantics of concept inclusion, if both $\langle C\sqsubseteq_{{\mathcal{O}}}D,d_{1}\rangle$, $\langle C\sqsubseteq_{{\mathcal{O}}}D,d_{2}\rangle$ hold, it suffices to keep only the concept inclusion with the maximum degree (similar for concept inclusions of the form $\langle C\sqsubseteq_{{\mathcal{O}}}\exists r.D,d\rangle$). For the same reason, a rule adding a concept inclusion $\langle C\sqsubseteq D, {d_{1}}\rangle$ to ${{\mathcal{O}}_{\rm SAT}}$ won’t be applied if ${{\mathcal{O}}_{\rm SAT}}$ already contains $\langle C \sqsubseteq D, {d_{2}}\rangle$ and d ₂ ≥ d ₁.

In Table 7 we use the relation $\rightsquigarrow$ (see rule CR6) between a nominal and a concept. The definition of this relation is similar to the one in Baader et al. (2005) adapted to membership degrees. For $\{a\},E \in BC_{{\mathcal{O}}}$ we say that $\langle \{ a\}\rightsquigarrow E,d\rangle$ when one of the following conditions holds:

• Either there exist concepts $\{C_{1},\ldots,C_{k+1}\}\subseteq BC_{{\mathcal{O}}}$ and roles $\{r_{1},\ldots,r_{k}\}\subseteq R_{{\mathcal{O}}}$, such that: (i) $\langle C_{i}{\kern-1pt}\sqsubseteq{\kern-1pt} \exists r_{i}.C_{i+1},d_{i}\rangle {\kern-1pt}\in{\kern-1pt} {{\mathcal{O}}_{\rm SAT}}$ for every 1 ≤ i ≤ k, (ii)  min (d ₁,...,d _k ) = d, (iii) C ₁ = { a} and C _k + 1 = E; or

• E is some nominal $\{ b\} \in BC_{{\mathcal{O}}}$ and d = 1. I.e. we have that $\langle \{ a\} \rightsquigarrow \{b\} ,1\rangle$ for every pair of nominals $\{ a\} ,\{ b\} \in BC_{{\mathcal{O}}}$.

Additionally, in rules CR7, CR8a, CR8b, CR9, $\overline{F}$ and $\overline{F}_{1}\ldots,\overline{F}_{m}$ correspond to vectors of feature names, while in rules CR7, CR8a, CR8b we consider that all the predicates belong to the same concrete domain $p_{1},\ldots,p_{m}\in\Phi^{{\mathcal{D}}}$, and that every concept inclusion $\langle C\sqsubseteq{p_{i}(\overline{F}_{i})},{d_{i}}\rangle$ concerning the particular concrete domain is taken into account. Finally rules CR8a, CR8b will only be applied if the resulting concept inclusion $\langle C\sqsubseteq{p(\overline{F})},d\rangle$ contains some concept $p(\overline{F})\in BC_{{\mathcal{O}}}$.

Theorem 1

(Correctness) Let ${\mathcal{O}}$ be a fuzzy ${\mathcal{EL}^{++}}$ ontology in normal form and let ${{\mathcal{O}}_{\rm SAT}}$ be obtained from ${\mathcal{O}}$ by exhaustively applying the rules of Table  7 until no new information is added to ${{\mathcal{O}}_{\rm SAT}}$ . For every nominal $\{ o\} \in BC_{{\mathcal{O}}}$ and concept $B\in BC_{{\mathcal{O}}}$ , ${\mathcal{O}}\models\langle \{ o\} \sqsubseteq B,d\rangle$ if and only if one of the following two conditions holds:

• S1 $\langle \{ o\} \sqsubseteq B,d^{\prime}\rangle \in{{\mathcal{O}}_{\rm SAT}}$ for some d′ ≥ d,

• S2 there exists some nominal $\{ a\} \in BC_{{\mathcal{O}}}$ such that $\langle \{ a\} \sqsubseteq\bot,d\rangle \in{{\mathcal{O}}_{\rm SAT}}$ and d > 0.

Example 10

Based on Example 3 we construct the ontology ${\mathcal{O}}=\langle \emptyset,C\cup\mathcal{C}_{{\mathcal{A}}}\rangle$ and then normalize it. The application of the Rules I1, I2, CR3,CR4 will be performed adding to the saturated ontology ${{\mathcal{O}}_{\rm SAT}}$ the following concept inclusions:

$$\begin{array}{rll} \langle \{ patient137\} &\sqsubseteq& \exists hasSeverityIndex.ASSIST0SeverityIndex,0.6\rangle \\ \langle \{ patient138\} &\sqsubseteq& \exists hasSeverityIndex.ASSIST0SeverityIndex,0.8\rangle \end{array}$$

Lemma 4

Fuzzy concept subsumption between a nominal {o } and a concept $B\in BC_{\mathcal{O}}$ w.r.t. some normalized fuzzy ${\mathcal{EL}^{++}}$ ontology ${\mathcal{O}}$ can be decided in polynomial time.

The following Theorem is an immediate consequence of Lemmata 2, 3 and 4.

Theorem 2

(Complexity) Fuzzy concept subsumption between fuzzy $\mathcal{EL}^{++}$ concepts can be decided in polynomial time.

6 Related work

There have been many works on extending the ${\mathcal{EL}}$ language with fuzzy set theory. Peter Vojtáš proposed a fuzzy extension of the $\mathcal{EL}$ language for performing queries containing several vague concepts of user’s preferences (Vojtáš 2007). The proposed language differs from usual fuzzy DL languages in that it interprets conjunction using fuzzy aggregation functions rather than t-norms. Also roles are not interpreted as fuzzy binary relations, bur rather as crisp (classical) ones. Stoilos et al. (2008) proposed a fuzzy extension of the $\mathcal{EL}^{+}$ language, using the operators of Gödel logic, which they named f _G -${\mathcal{EL}^{+}}$. The language introduced in this paper is an extension of the one presented in Stoilos et al. (2008), with nominals, the bottom concept, and fuzzy concrete domains. The language f _G -${\mathcal{EL}^{+}}$, was used by Feng et al. (2010), for computing logical differences between ontologies. Finally, Vanekov et al. propose in Vaneková and Vojtáš (2010) a fuzzy ${\mathcal{EL}}\left({\mathcal{D}}\right)$ language which extends the language presented in Vojtáš (2007) with the aggregation constructor @ _U , the top-k constructor, and fuzzy concrete domains. The aggregation constructor allows to define the degree of some concept based on some aggregation function and the degrees of a set of concepts. The top-k constructor allows to select from a concept C only the k individuals with the highest degrees, while the proposed concrete domain allows for linguistic variables such as good _Price etc. that are based on some membership function.

The main differences between our language and the language presented in Vaneková and Vojtáš (2010) which also allows for fuzzy concrete domains are the following: The language presented in Vaneková and Vojtáš (2010) provides for the aggregation @ _U and the top-k constructor while it considers only for crisp roles. On the other hand, the language we propose supports for nominals, the bottom concept, role composition and fuzzy roles. Another difference is that the language presented in Vaneková and Vojtáš (2010) due to the presence of the aggregation @ _U and the top-k constructor is non-monotonic in contrast to our language that preserves monotonicity. Finally we should notice that the complexity of the language presented in Vaneková and Vojtáš (2010) has not yet been studied.

Regarding fuzzy concrete domains, our work is based on works of Straccia and Bobillo. In Straccia (2005a), Straccia first introduced the notion of a fuzzy concrete domain, ${\mathcal{D}}=\langle \Delta_{{\mathcal{D}}},\Phi_{{\mathcal{D}}}\rangle$, where $\Delta_{\mathcal{D}}$ is the interpretation domain and $\Phi_{\mathcal{D}}$ is the set of fuzzy concrete domain predicates. In order to provide a link between fuzzy concrete domains and the DL fuzzy $\mathcal{ALC}({\mathcal{D}})$, Straccia provides the constructors $\forall T.D,\ \exists T.D$ where T is a concrete role and D is either some unary fuzzy concrete domain predicate d, or its negation $\neg d$. Reasoning in $\mathcal{ALC}({\mathcal{D}})$, is performed by reduction to bounded mixed integer programming (bMIP) (Hahnle 2001). The work is extended by Bobillo and Straccia (2009b) with the additional constructors ( ≥ t n), ( ≤ t n), ( = t n), where t is some concrete feature name and n some value in the interpretation domain $\Delta^{\mathcal{D}}$. Finally Bobillo and Straccia (2009a) further extend the language $\mathcal{ALC}({\mathcal{D}})$ with mathematical operations either between real numbers, or between fuzzy membership functions such as fuzzy numbers. The proposed language allows to define new membership functions. For example we can define the datatype that is the result of adding the membership functions of two different triangular functions.

Even though the expressive power of the language proposed by Bobillo and Straccia is appealing, fuzzy ${\mathcal{EL}^{++}}$ cannot embody arbitrary fuzzy concrete domains that do not comply with the restrictions presented in Definitions 1 and 2. In fact, in Example 7 we showed how fuzzy ${\mathcal{EL}^{++}}$ expanded with a simple concrete domain on the rational numbers and fuzzy predicates based on the triangular membership function can change the complexity of the fuzzy ${\mathcal{EL}^{++}}$ language to non-polynomial. Therefore the main contribution, w.r.t. previous work on fuzzy concrete domains, is that our paper presents the admissibility restrictions that ensure that the fuzzy ${\mathcal{EL}^{++}}$ language retains its polynomial complexity.

7 Conclusions and future work

In this paper we have presented a fuzzy extension of the DL language $\mathcal{EL}^{++}$, creating fuzzy $\mathcal{EL}^{++}$. We first described its syntax and semantics, while then we showed how each inference problem of fuzzy DLs, i.e. concept satisfiability, ontology consistency and instance checking, can be reduced to the fuzzy concept subsumption problem. Subsequently, we have developed a tractable algorithm for deciding the fuzzy subsumption problem. Compared to previous approaches our language supports nominals, the bottom concept, and fuzzy concrete domains. Nominals allow for reasoning w.r.t. assertional knowledge (which cannot be done in e.g. fuzzy-$\mathcal{EL}^{+}$), while the presence of the bottom concept allows to express disjointness between concepts (e.g. $\langle C\sqcap D\sqsubseteq\bot,1\rangle$), and together with nominals, to express difference between individuals (e.g. $\langle \{ a\} \sqcap\{ b\} \sqsubseteq\bot,1\rangle$). Moreover, the fuzzy concrete domains of fuzzy ${\mathcal{EL}^{++}}$ allow the representation of concrete qualities of real-world objects such as their weight, temperature, and spatial extension. Finally, we provided detailed proofs of the correctness of the presented reasoning algorithm.

Regarding future work, we plan to extend the semantics of the fuzzy ${\mathcal{EL}^{++}}$ language to allow for arbitrary t-norm operators for interpreting conjunction. Having in mind the latest work of Baader and Peñaloza (2011), which proves undecidability for a specific family of fuzzy DL languages extended with arbitrary t-norms, it is interesting to investigate if the same will apply for the fuzzy ${\mathcal{EL}^{++}}$ language. If such is the case, it is interesting to examine decidable and polynomial sublanguages of the fuzzy ${\mathcal{EL}^{++}}$ language extended with general t-norms. Finally, we also want to consider more expressive, but still tractable, logics than ${\mathcal{EL}^{++}}$. Such logics have also been investigated in the literature (Baader et al. 2008) and they allow for constructors such as domain and range restrictions on roles.

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.