A fuzzy spatial description logic for the semantic web

Abstract

Spatial information is a critical feature in a large number of application domains. Spatial information, however, is often not crisp but with the nature of imprecision and fuzziness. As the increasing requirements of spatial applications, there emerges many challenges regarding to the representation and reasoning of spatial knowledge. Description logic (DL) is a logical basis for representing knowledge and realizing reasoning tasks in the Semantic Web. Therefore, how to extend DL to achieve the goal of representing and reasoning fuzzy spatial knowledge needs to be settled. In this work, we study a fuzzy spatial extension of the well known fuzzy $\mathcal {ALC}$ DL to reason fuzzy spatial knowledge. First, we construct a fuzzy spatial concrete domain $\mathcal {S}$ which is comprised of fuzzy spatial regions and fuzzy RCC relationships. More importantly, we give the admissibility proof of fuzzy spatial concrete domain $\mathcal {S}$. Then we extend fuzzy $\mathcal {ALC}$ with an admissible fuzzy spatial concrete domain $\mathcal {S}$ and present a fuzzy spatial description logic f-${\mathcal {ALC}}({\mathcal S})$. Finally, we address a decision procedure for f-${\mathcal {ALC}}({\mathcal S})$ ABox consistency problem. Also, we show that the decision procedure is correct and the consistency problem for f-${\mathcal {ALC}}({\mathcal S})$ is decidable in PSPACE-complete.

1 Introduction

Currently, spatial information is commonly found in many different application fields such as spatial database systems, Geographical information system (GIS), and meteorological analysis (Rigaux et al. 2001; Belussi and Migliorini 2012). As the increasing requirements of spatial applications, an important research domain called spatial knowledge management emerges. Therefore, there emerge many challenges regarding to the management of fuzzy spatial knowledge, which includes representation, reasoning, and instance retrieval (Torres-Ruiz et al. 2016; Mousavi et al. 2018; Xu et al. 2019).

However, there exist the problems of information imprecision and uncertainty in many spatial application domains. In other words, fuzziness can be found in the spatial information as well as spatial topological relationships (Schneider 1999). For example, in an environmental and meteorological system, the boundary of a hurricane is fuzzy (Cheng 2016). The ubiquitous existence of fuzzy spatial information has attracted interests of researchers in the areas of robot vision, visual object tracking, multimedia, and GIS (Ribaric and Hrkac 2012). They investigate techniques to represent and reason the fuzzy spatial information (Cheng et al. 2019b).

Recently, some large-scale fuzzy spatial knowledge and the corresponding applications have been introduced into the Semantic Web. Description logics (short for DLs), as a logical basis for representing knowledge and realizing reasoning tasks in the Semantic Web, have become a hot research issue in the areas of software engineering, computer science, and artificial intelligence (Haarslev et al. 1999; Straccia 2001; Lu et al. 2018). One of motivations for extending $\mathcal {ALC}$ in that way is to augment description logic $\mathcal {ALC}$ with some kind of fuzzy spatial reasoning capabilities. Consider an example (modeling fuzzy spatial relations) consisting of three spatial regions X, Y, and Z. They have some spatial relations such as “region X is disconnected with region Y with a degree of 0.4, region Z is part of region Y with a degree of 0.8”. Let us consider another example: given a specific city (Hangzhou) and a lake (Westlake), the concept “all districts in the city which are overlapped by the lake with a degree of 0.6”. We wish to have a description logic which allows us to represent and reason fuzzy spatial relations in this manner. Hence, how to extend description logic to achieve the goal of representing and reasoning fuzzy spatial knowledge needs to be settled.

Existing work on representation and reasoning of spatial knowledge extends the presentation capabilities of DLs. Multiple forms of DLs are proposed for different applications, such as ${\mathcal {ALC}}({\mathcal S})$ (Lutz 2002b), ${\mathcal{ALCRP}}({\mathcal{S}}_2)$ (Haarslev et al. 1999), $\mathcal {ALCRP}^3(DcCOA)$ (Kaplunova et al. 2002), ${\mathcal {ALC}}({\mathcal C})$ (Lutz and Brandt 2007), $\mathcal {ALCI}_{RCC}$ family (Wessel 2002), $\mathcal {ALC}_s$ (Wang and Liu 2008) and ${\mathcal {ALC}}({\mathcal CDC})$ (Cristani and Gabrielli 2009). However, the above methods only apply for reasoning crisp spatial knowledge. To support reasoning fuzzy spatial knowledge, Straccia (2009) proposes a fuzzy extension of crisp description logics called fuzzy ${\mathcal {ALC}}({\mathcal D})$ which introduces a fuzzy concrete domain including classic regions and their spatial topological relations and allows the reasoning of fuzzy spatial relationships. Unfortunately, the author assumes that the concrete domain is admissible and does not provide the proof of admissibility. At the same time, the correctness (termination, soundness, and completeness) of reasoning algorithm is not proved and the complexity of the reasoning problems is not analyzed. To support spatial topological relations reasoning in the field of medical imaging, Hudelot et al. (2010, 2014) present a new description logic called ${\mathcal {ALC}}({\mathcal F})$ which uses a fuzzy mathematical morphology method to define a concrete domain. Although the reasoning algorithm of ${\mathcal {ALC}}({\mathcal F})$ is given, the inference of fuzzy abstract concept knowledge is not considered and the correctness of the reasoning algorithm is not proved. The comprehensive review of crisp and fuzzy spatial description logics can be found in Sect. 2.

This paper proposes a DL-based approach for representing and reasoning fuzzy Region Connection Calculus (short for RCC) relations. By extending fuzzy DLs fuzzy $\mathcal {ALC}$ (Straccia 2001) with fuzzy spatial concrete domains $\mathcal {S}$, we address a fuzzy spatial extension of description logic f-${\mathcal {ALC}}({\mathcal S})$. Briefly, the paper makes four contributions as follows:

• We construct a fuzzy spatial concrete domain $\mathcal {S}$ which is comprised of fuzzy spatial regions and fuzzy RCC relationships. Then, we prove that $\mathcal {S}$ is admissible.

• We extend the well known and basic DL fuzzy $\mathcal {ALC}$ with an admissible fuzzy spatial concrete domain $\mathcal {S}$ and then propose a fuzzy spatial description logic f-${\mathcal {ALC}}({\mathcal S})$. We investigate a formal definition of f-${\mathcal {ALC}}({\mathcal S})$ three core components including syntax structure, semantic interpretation, and knowledge base.

• We address a decision procedure for f-${\mathcal {ALC}}({\mathcal S})$ to decide f-${\mathcal {ALC}}({\mathcal S})$ ABox consistency. At the same time, we give an example to illustrate how to decide the consistency of the f-${\mathcal {ALC}}({\mathcal S})$ ABox with our tableau algorithm.

• We prove that the tableau-based decision procedure is correct (termination, soundness, and completeness) and analyze simply the complexity of the reasoning problem with f-${\mathcal {ALC}}({\mathcal S})$.

The rest of the paper is organized as follows. Section 2 reviews the related work. In Sect. 3, we give the basic knowledge about fuzzy sets theory, fuzzy description logic, and fuzzy region connection calculus (f-RCC), as far as they are relevant to this paper. In Sect. 4, we define a fuzzy spatial concrete domain $\mathcal {S}$ and show the admissibility of concrete domain $\mathcal {S}$. In Sect. 5, we address a fuzzy description logic f-${\mathcal {ALC}}({\mathcal S})$ supporting the reasoning of fuzzy RCC spatial relations. In Sect. 6, we attempt to discuss the reasoning algorithm of f-${\mathcal {ALC}}({\mathcal S})$. Our conclusions are provided in the final section.

2 Related work

A fuzzy spatial description logic f-${\mathcal {ALC}}({\mathcal S})$ is a fuzzy spatial concrete domain extension of fuzzy description logic. The most important application area is fuzzy spatial knowledge reasoning. The related works concerning the proposed fuzzy spatial description logic can be classified into two main categories: (i) crisp spatial description logic, (ii) fuzzy spatial description logic. The descriptions of the related works are introduced in the following.

The first category is crisp spatial description logic. In recent years, many strategies have been proposed to represent and reason crisp spatial knowledge with description logics. A lot of work has been carried out toward extending the classical $\mathcal {ALC}$ (Schmidt-Schau and Smolka 1991) with concrete domains. In (Baader and Hanschke 1991), a basic description logic named ${\mathcal {ALC}}({\mathcal D})$ is presented. The ${\mathcal {ALC}}({\mathcal D})$ can integrate $\mathcal {ALC}$ reasoning with reasoning about concrete domains $\mathcal {D}$, where concrete domains consist of two parts: (i) a set of concrete objects; (ii) a set of predicates (e.g., unary or binary predicates) defined over these objects. Lutz (2002b) defines a spatial concrete domain $\mathcal {S}$ based on RCC-8 relations (Randell et al. 1992) and shows that $\mathcal {S}$ is admissible and $\mathcal {S}$-satisfiability is a NP problem. Then, the author proposes a description logic ${\mathcal {ALC}}({\mathcal S})$ by extending classical $\mathcal {ALC}$ with the spatial concrete domain $\mathcal {S}$. On this basis, Haarslev et al. (1999) propose a description logic ${\mathcal{ALCRP}}({\mathcal{S}}_2)$ which extends ${\mathcal {ALC}}({\mathcal S})$ with a role-forming predicate operator. The ${\mathcal{ALCRP}}({\mathcal{S}}_2)$ can support the reasoning of spatial objects and their qualitative RCC-8 spatial relations. Moreover, Lutz (2002b) points out that the satisfiability of ${\mathcal{ALCRP}}({\mathcal{S}}_2)$ concept is in NEXPTIME. Based on ${\mathcal{ALCRP}}({\mathcal{S}}_2)$, Kaplunova et al. (2002) discuss the spatial description logic called $\mathcal {ALCRP}^3(DcCOA)$, where the concrete domain DcCOA is composed of spatial points, cardinal direction relations, and relative orientation relations. In the case of decidability, the consistency of $\mathcal {ALCRP}^3(DcCOA)$ ABox is undecidable. If the $\mathcal {ALCRP}^3(DcCOA)$ concepts and roles are defined in the form of syntax-restriction, then the consistency problem is also decidable. The most obvious difference between $\mathcal {ALCRP}^3(DcCOA)$ and ${\mathcal{ALCRP}}({\mathcal{S}}_2)$ is that ${\mathcal{ALCRP}}({\mathcal{S}}_2)$ does only support the binary spatial topological roles whereas $\mathcal {ALCRP}^3(DcCOA)$ can represent ternary spatial topological relationships and direction relationships. Na et al. (2006) give the definition of some new spatial predicates of spatial concrete domains based on ${\mathcal {ALCRP}}({\mathcal D})$ according to the requirement of multimedia information retrieval. These predicates mainly describe spatial topological relations between line and region. The foundation of the spatial topological relations is a set of the nine-intersection model that includes 19 different situations. However, a decidable reasoning procedure for the reasoning problem is not provided.

There have also been many proposals to extend description logic $\mathcal {ALC}$ with constraint systems for the reasoning of spatial knowledge. By combining a constraint system and general TBox with a classical DL $\mathcal {ALC}$, Lutz and Brandt (2007) propose a description logic ${\mathcal {ALC}}({\mathcal C})$ with a constraint system C which is based on RCC-8 spatial relations and also prove the C is $\omega$-admissible. A sound and complete decision procedure for solving the satisfiability problem of ${\mathcal {ALC}}({\mathcal C})$ concept w.r.t general TBox is provided. On this basis, Cristani and Gabrielli (2009) address a new description logic ${\mathcal {ALC}}({\mathcal CDC})$ obtained by combining a description logic ${\mathcal {ALC}}({\mathcal C})$ with Cardinal Direction Calculus ($\mathcal {CDC}$). The $\mathcal {CDC}$ is $\omega$-admissible constraint system that studies points in a two-dimensional space and their cardinal direction relations. For example, relations between points include northwest, northeast, southwest, southeast, north, east, west, and south. Similar to ${\mathcal {ALC}}({\mathcal C})$, the ${\mathcal {ALC}}({\mathcal CDC})$ is also decidable.

In addition to the combination of description logic $\mathcal {ALC}$ with concrete domain or constraint systems, several works for extending $\mathcal {ALC}$ with composition table have been done. Wessel (2002) presents a family of $\mathcal {ALCI}_{RCC}$ languages that extend $\mathcal {ALC}$ with RCC composition tables such as RCC-5 and RCC-8. In $\mathcal {ALCI}_{RCC}$ family, a spatial relation can be considered as a role at an abstract level and this role is originated from the corresponding RCC composition tables. The decidability of satisfiability of $\mathcal {ALCI}_{RCC}$ concept is also proved. For example, $\mathcal {ALCI}_{RCC1}$, $\mathcal {ALCI}_{RCC2}$, and $\mathcal {ALCI}_{RCC3}$ are decidable. But, for $\mathcal {ALCI}_{RCC5}$ and $\mathcal {ALCI}_{RCC8}$, the decidability is not known. Wang and Liu (2008) propose a spatial description logic $\mathcal {ALC}_s$ in the context of geospatial Semantic Web. The proposed spatial description logic views RCC-8 spatial relationships as a kind of concepts, not roles. Moreover, using $\mathcal {ALC}_s$, the constraint satisfaction problem for RCC-8 can be solved in EXPTIME-complete time.

In real-world applications, spatial knowledge is often fuzzy/vague/uncertain (Cheng 2016; Singh and Soni 2019). The classical description logic languages are not suitable to deal with this knowledge. Hence, fuzzy spatial description logics emerge as useful in GIS systems, image system, and spatial database system (Zhang et al. 2018; Lu et al. 2019).

The second category is fuzzy spatial description logic. Currently, there have been several works investigating fuzzy spatial description logics. Straccia (2009) proposes a novel approach to extend fuzzy description logic ${\mathcal {ALCF}}({\mathcal D})$ (Straccia 2005, 2006) with a fuzzy spatial concrete domain, and develops a fuzzy ${\mathcal {ALC}}({\mathcal D}).$ This fuzzy spatial concrete domain is composed of the classic spatial region and fuzzy RCC-8 spatial topological predicates. Similar to our approach, the fuzzy spatial concrete domain is also needed. At the same time, the author proposes a reasoning algorithm for determining Best Satisfiability Degree and Best Entailment Degree of knowledge base. Although the authors give a definition of a fuzzy concrete domain, they only assume that the concrete domain is admissible. Our paper differs from them that we show the admissibility of concrete domain and provide a decision approach of satisfiability of concrete domain. Also, in fuzzy ${\mathcal {ALC}}({\mathcal D})$, the correctness (termination, soundness, and completeness) of reasoning algorithm is not proved and the complexity of the reasoning problems is not analyzed. Please note that our paper is inspired by the work proposed by Straccia (2009). To achieve spatial reasoning in the domain of medical imaging, Hudelot et al. (2010, 2014) present a novel DL called ${\mathcal {ALC}}({\mathcal F})$, which is based on the combination of ${\mathcal {ALCRP}}({\mathcal D})$ (Haarslev et al. 1999) and spatial concrete domain $\mathcal {F}$. The concrete domain mainly contains distance relations and spatial relations (e.g., close to, left, to the right of) which are defined using a fuzzy mathematical morphology approach. Furthermore, the authors give a decision procedure for dealing with fuzzy spatial topological relations. But, the ${\mathcal {ALC}}({\mathcal F})$ only focuses on the fuzzy spatial domain but does not take fuzzy concepts into consideration. The decidability for ${\mathcal {ALC}}({\mathcal F})$ equipped with fuzzy spatial relations is also not proved. Based on the temporal extension of fuzzy description logic fuzzy ${\mathcal {ALC}}({\mathcal D})$ proposed by Straccia (2009), Cheng and Ma (2017, 2019) present a fuzzy spatio-temporal description logic f-${\mathcal {ALC}}({\mathcal D})$-LTL to support fuzzy spatio-temporal reasoning. In f-${\mathcal {ALC}}({\mathcal D})$-LTL, fuzzy ${\mathcal {ALC}}({\mathcal D})$, as a foundation for the whole spatio-temporal reasoning work, determines different spatial knowledge reasoning.

For the detailed review about crisp and fuzzy spatial description logics, please refer to Cheng et al. (2019a).

3 Preliminaries

In this section, we briefly recapitulate some necessary preliminaries needed during the rest of the paper. Section 3.1 recalls some notions of fuzzy sets theory. Section 3.2 introduces the basic notion of fuzzy description logic, and Sect. 3.3 summarizes fuzzy region connection calculus.

3.1 Fuzzy sets theory

The concept of fuzzy sets was first proposed by Zadeh (1965), which is an extension of the classical concept of set. Fuzzy sets and fuzzy logic theory provide a convenient way to describe fuzzy/vague/imprecise concepts that exist in real-world applications (George J and Bo 1995; Ma et al. 2014; Garg and Arora 2020).

Suppose that U is a collection of elements, a fuzzy set A (Zadeh 1965) in U is characterized by a membership function $\mu _A(x)$:$U\rightarrow$ [0, 1], or $A(x):U\rightarrow$ [0, 1]. The function assigns each element $x\in U$ to a value in the unit [0, 1], i.e., $A(x)\in$ [0, 1]. The value of A(x) represents the degree of truth of the fact that x belongs to U. For example, A(x) = 0.4 means that x belongs to U with a degree of 0.4. The support set of a fuzzy set A is a crisp set $sup(A) = \{x \mid A(x) > 0\}$.

A fuzzy binary relation R in $U\times U$ is a function $R: U\times U\rightarrow$ [0, 1]. For a and b in U, R(a, b) is the degree of strength of the association between a and b. For instance, Is-a(a, b) = 0.3 means that the object a is an object b to a degree of 0.3. For the detail of some properties of the fuzzy binary relation, we refer the reader to George J and Bo (1995).

In fuzzy logic, there are four logical operators called negation ($\ominus$), t-norm ($\otimes$), implication ($\Rightarrow$), and t-conorm ($\oplus$), which are fuzzy extensions of classical logical operators. Also, four popular families of fuzzy logics, namely, Zadeh (1965), Gödel, Łukasiewicz, and Product logics (Hájek 2001) are typically used. Zadeh logic is entailed by Łukasiewicz logic. Zadeh logic: $a\otimes b$ = min(a, b), $a\oplus b$ = max(a, b), $\ominus a$ = 1-a, and $a\Rightarrow b$ = max(1-a, b) for $a, b\in [0, 1]$. Łukasiewicz logic: $a\otimes b$ = max($a+b$-1, 0), $a\oplus b$ = min($a+b$, 1), $\ominus a$ = 1-a, and $a\Rightarrow b$ = min(1-a+b, 1) for $a, b\in [0, 1]$. In particular, the residual fuzzy implication is also typically used in terms of t-norm. It can be defined as $a\Rightarrow _rb$ = sup{$\lambda \in [0, 1]\mid a\otimes \lambda \le b$} for $a, b\in [0, 1]$.

3.2 Fuzzy description logic

Fuzzy description logic (fuzzy $\mathcal {ALC}$) is considered as a basic description logic extended with fuzzy set theory (Straccia 2001; Bobillo and Straccia 2009; Bobillo et al. 2011). The purpose of fuzzy $\mathcal {ALC}$ is to capture fuzzy knowledge, establish declarative semantics and provide a decidable reasoning service (Hájek 2005; Straccia 2006). Complex concepts in fuzzy $\mathcal {ALC}$ can be defined by atomic concepts and atomic roles. The syntax rule is represented as below:

$$\begin{aligned} C, D \rightarrow \top \mid \perp \mid A \mid \lnot C \mid C\sqcap D \mid C\sqcup D \mid \forall R.C \mid \exists R.C, \end{aligned}$$

where C and D represent concepts, A and R represent atomic concepts and atomic roles, respectively.

The semantics of fuzzy $\mathcal {ALC}$ DL are based on fuzzy interpretations $\mathcal {I}$=$(\Delta ^{\mathcal {I}}, \bullet ^{\mathcal {I}})$, where $\Delta ^{\mathcal {I}}$ is an interpretation domain with nonempty set and $\bullet ^{\mathcal {I}}$ is a fuzzy interpretation function. In fuzzy $\mathcal {ALC}$, the fuzzy interpretation assigns to each concept name C a function $C^{\mathcal {I}}:\Delta ^{\mathcal {I}}\rightarrow$[0, 1] and to each role name R a function $R^{\mathcal {I}}:\Delta ^{\mathcal {I}}\times \Delta ^{\mathcal {I}}\rightarrow$[0, 1]. The fuzzy interpretation $\bullet ^{\mathcal {I}}$ can be extended to complex concepts by the following definitions (where $a\in \Delta ^{\mathcal {I}}$).

$$\begin{aligned}&\top ^{\mathcal {I}}(a)=1 \\&\bot ^{\mathcal {I}}(a)=0\\&(\lnot C)^{\mathcal {I}}(a)=\ominus C^{\mathcal {I}}(a)\\&(C\sqcap D)^{\mathcal {I}}(a)=C^{\mathcal {I}}(a) \otimes D^{\mathcal {I}}(a)\\&(C\sqcup D)^{\mathcal {I}}(a)=C^{\mathcal {I}}(a) \oplus D^{\mathcal {I}}(a)\\&(\forall R.C)^{\mathcal {I}}(a)= inf_{b\in {\Delta ^{\mathcal {I}}}} \{ \ominus R^{\mathcal {I}}(a,b)\oplus C^{\mathcal {I}}(b)\}\\&(\exists R.C)^{\mathcal {I}}(a)= sup_{b\in {\Delta ^{\mathcal {I}}}} \{ R^{\mathcal {I}}(a,b)\otimes C^{\mathcal {I}}(b)\} \end{aligned}$$

Please note that a fuzzy knowledge base $\mathcal {K}$ is composed of two core parts, namely, a fuzzy TBox $\mathcal {T}$ and a fuzzy Abox $\mathcal {A}$. A fuzzy TBox $\mathcal {A}$ is a finite collection of fuzzy concept inclusion axioms in the form of $C\sqsubseteq D$ and $C=D$. For the semantics of terminology axioms appearing in $\mathcal {T}$, there are: $C\sqsubseteq D$ iff $\forall a\in \Delta ^{\mathcal {I}}, C^{\mathcal {I}}(a)\le D^{\mathcal {I}}(a)$; $C=D$ iff $D\sqsubseteq C$ and $C\sqsubseteq D$, i.e., $\forall a\in \Delta ^{\mathcal {I}}, C^{\mathcal {I}}(a) = D^{\mathcal {I}}(a)$. A fuzzy interpretation $\mathcal {I}$ satisfies a fuzzy TBox $\mathcal {T}$ iff it satisfies each terminology axioms in $\mathcal {T}$; in the condition, $\mathcal {I}$ is called a model of $\mathcal {T}$, denoted $\mathcal {I} \models \mathcal {T}$. A fuzzy ABox $\mathcal {A}$ is a finite set of fuzzy assertions of the forms $\langle a:C \bowtie n\rangle$ and $\langle (a,b):R \bowtie n \rangle$, where $n\in$ [0, 1], and $\bowtie$ stands for $>, \ge ,<$ and $\le$ or of the form $a \ne b$. Given a fuzzy interpretation $\mathcal {I}$, for the semantics of assertions in $\mathcal {A}$, we have:

• $\mathcal {I}$ satisfies $\langle a:C \bowtie n\rangle$ iff $C^{\mathcal {I}}(a^{\mathcal {I}})\bowtie n$,

• $\mathcal {I}$ satisfies $\langle (a,b):R \bowtie n \rangle$ iff $R^{\mathcal {I}}(a^{\mathcal {I}},b^{\mathcal {I}})\bowtie n$,

• $\mathcal {I}$ satisfies $a \ne b$ iff $a^{\mathcal {I}}\ne b^{\mathcal {I}}$.

A fuzzy interpretation $\mathcal {I}$ satisfies fuzzy ABox $\mathcal {A}$ iff it satisfies each fuzzy assertions in $\mathcal {A}$.

Fuzzy $\mathcal {ALC}$ offers a set of reasoning services. The basic reasoning tasks of fuzzy $\mathcal {ALC}$ include Concept satisfiability, Concept subsumption, ABox consistency, and Knowledge Base satisfiability. For the detail of the introduction, we refer the reader to Straccia (2015). It should be noted that ABox consistency is one key problem in the process of fuzzy $\mathcal {ALC}$ reasoning. All of the above reasoning tasks can be reduced to ABox consistency (Straccia 2006). In order to decide the consistency, the most widely used reasoning technique is based on tableau algorithm (Lutz and Brandt 2007).

3.3 Fuzzy Region connection calculus

The Fuzzy Region Connection Calculus (f-RCC) (Schockaert et al. 2008a, b, 2009), as a is an extension of crisp RCC (Randell et al. 1992), denotes fuzzy spatial topological relations between fuzzy regions. Similarly to crisp RCC, f-RCC topological relations are also based on a reflexive and symmetric relation C(a, b), called connection, where a and b represent two fuzzy regions. The fuzzy region is based on fuzzy point set, while the fuzzy relation C is based on the nearness degree between the fuzzy sets. Using t-norm and residual fuzzy implication in Łukasiewicz Logic, RCC topological relations can be extended to fuzzy RCC relations. In fuzzy RCC, C is a fuzzy relation. For arbitrary two fuzzy regions a and b, the topological relation C(a, b) represents the degree to which a is connected with b, $C(a, b)\in [0, 1]$. The other fuzzy RCC topological relations can be defined in term of fuzzy relation C. Table 1 shows the definitions of crisp RCC and fuzzy RCC.

Table 1 Definitions of crisp RCC and fuzzy RCC for regions a and b (Schockaert et al. 2009, 2010)

It should be noted that fuzzy relations DC, PP, DR, PO, EC, TPP and NTPP are non-reflexive, while fuzzy relations P, EQ, and O are reflexive. For more detailed information about fuzzy RCC, it can be found in Schockaert et al. (2008a, b, 2009).

4 Fuzzy spatial concrete domain $\mathcal {S}$

In order to develop a fuzzy description logic supporting fuzzy spatial reasoning, it is necessary to define fuzzy spatial concrete domain that allows to deal with fuzzy spatial regions and their fuzzy RCC relations. We first define the underlying notion of a fuzzy spatial concrete domain $\mathcal {S}$ (see Sect. 4.1). Then, we show the admissibility of this concrete domain $\mathcal {S}$ (see Sect. 4.2) and provide a decision approach of fuzzy spatial concrete domain (see Sect. 4.3).

4.1 Formal definition

Before giving the formal definition of fuzzy spatial concrete domain $\mathcal {S}$, we first briefly introduce fuzzy concrete domain.

Definition 1

(Fuzzy concrete domain) Straccia (2005), Merz et al. (2014) A fuzzy concrete domain $\mathcal {D}$ is a tuple $(\Delta _{\mathcal {D}}, \Phi _{\mathcal {D}})$, where $\Delta _{\mathcal {D}}$ is an interpretation domain and $\Phi _{\mathcal {D}}$ is the set of fuzzy predicates d with a predefined arity n and an interpretation $d^{\mathcal {D}}$: $\Delta _{\mathcal {D}}^n \rightarrow [0, 1]$, which is a n-ary fuzzy relation over $\Delta _{\mathcal {D}}$.

Based on the Definition 1 and fuzzy RCC relations discussed by Schockaert et al. (2008a, b, 2009), we give a formal definition of fuzzy spatial concrete domain $\mathcal {S}$.

Definition 2

(Fuzzy spatial concrete domain) A fuzzy spatial concrete domain $\mathcal {S}$ is a pair $(\Delta _{\mathcal {S}}, \Phi _{\mathcal {S}})$, where:

• $\Delta _{\mathcal {S}}$ is a set of region variables from universe of regions U

• $\Phi _{\mathcal {S}}$ is a set of binary fuzzy spatial predicates r; arbitrary binary predicate $r\in \Phi _{\mathcal {S}}$ is a binary fuzzy relations $r^{\mathcal {S}}$:$\Delta _{\mathcal {S}}\times \Delta _{\mathcal {S}} \rightarrow$[0, 1] over $\Delta _{\mathcal {S}}$. Here, r consists of two kinds of fuzzy spatial predicates: (i) fuzzy RCC relation (also called atomic fuzzy RCC relation) and (ii) fuzzy RCC expression built from a Boolean combination of atomic fuzzy RCC relations. So, the set $\Phi _{\mathcal {S}}$ of binary fuzzy spatial predicates r contains a set of fuzzy RCC relations and a set of fuzzy RCC expressions.

Fuzzy RCC relations are fuzzy relation C and other fuzzy topological relations (DC, TPP, P, PO, PP, DR, EC, O, EQ, NTP, NTTP) as from Table 1. From the perspective of semantics, on one hand, a fuzzy interpretation function $\bullet ^{\mathcal {S}}$ maps an atomic fuzzy RCC relation predicate $C\in \Phi _{\mathcal {S}}$ into a fuzzy relation $C^{\mathcal {S}}$: $\Delta _{\mathcal {S}} \times \Delta _{\mathcal {S}}\rightarrow [0, 1]$ over $\Delta _{\mathcal {S}}$. On the other hand, according to the literature (Schockaert et al. 2009), the interpretations of the other atomic fuzzy RCC predicates $r\in$ {DC, TPP, P, PO, PP, DR, EC, O, EQ, NTP, NTTP)} can be extended by the interpretation of C. The extension is based on the definitions of fuzzy RCC relations in Table 1.

For examle, we can extend the interpretation of C to interpret fuzzy RCC predicate P, i.e., $P^{\mathcal {S}}(a,b)$ = $inf_{c\in U}(C^{\mathcal {S}}(c,a)\Rightarrow _{r}C^{\mathcal {S}}(c,b))$.

A fuzzy RCC expression is a boolean combination of fuzzy RCC relations. These Boolean operators include conjunction, disjunction, implication, and negation. In the following, we define fuzzy RCC expressions.

Definition 3

(Fuzzy RCC expression) A fuzzy RCC expression $\mathbf{r} \in \Phi _{\mathcal {S}}$ can be built inductively from the following syntactic rules:

$$\begin{aligned} \mathbf{r} {:}{:}{=}\,\,\,r(a,b)\mid \lnot \mathbf{r} \mid \mathbf{r} _1\vee \mathbf{r} _2 \mid \mathbf{r} _1\wedge \mathbf{r} _2 \mid \mathbf{r} _1\rightarrow \mathbf{r} _2 \end{aligned}$$

where, $r\in \Phi _{\mathcal {S}}$ is either fuzzy RCC relation C or one of fuzzy RCC relations from Table 1(DC, TPP, P, PO, PP, DR, EC, O, EQ, NTP, NTTP), a and b are arbitrary two region variables over $\Delta _{\mathcal {S}}$.

For example, $P(a,b)\vee C(a,b)$(also denoted as $(P\vee C)(a,b)$) and $NTPP(a, b)\wedge PO(a,c)$ are two fuzzy RCC expressions.

To interpret the fuzzy RCC expressions, we need to transform fuzzy RCC expressions into a set of atomic fuzzy RCC relations. That means, at first, every fuzzy RCC expression can be written equivalently as a finite set of fuzzy RCC relationships without quantifiers. Then, we extend the interpretation of fuzzy topological relation C to interpret fuzzy RCC relations (DC, TPP, P, PO, PP, DR, EC, O, EQ, NTP, NTTP)

Based on fuzzy sets and Zadeh logic (Zadeh 1965), a fuzzy interpretation function $\bullet ^{\mathcal {S}}$ can be extended to fuzzy RCC expressions by the following definitions (where, $a, b\in \Delta _{\mathcal {S}}$ denote two region variables):

• (1) $\mathbf{r} ^{\mathcal {S}}=\mu \in$[0, 1] for $\mathbf{r} = r$ denotes atomic fuzzy RCC relations,

• (2) $(\lnot \mathbf{r} )^{\mathcal {S}}=\ominus \mathbf{r} ^{\mathcal {S}}$,

• (3) $(\mathbf{r} _1 \vee \mathbf{r} _2)^{\mathcal {S}}=\mathbf{r} _1^{\mathcal {S}} \oplus \mathbf{r} _2^{\mathcal {S}}$,

• (4) $(\mathbf{r} _1 \wedge \mathbf{r} _2)^{\mathcal {S}}=\mathbf{r} _1^{\mathcal {S}} \otimes \mathbf{r} _2^{\mathcal {S}}$,

• (5) $(\mathbf{r} _1 \rightarrow \mathbf{r} _2)^{\mathcal {S}}=\mathbf{r} _1^{\mathcal {S}} \Rightarrow \mathbf{r} _2^{\mathcal {S}}$.

For example, using the above interpretation and the definitions from Table 1, we give the semantics of fuzzy RCC expression $P(a, b) \vee C(a, b)$ as follows:

$$\begin{aligned}&(P(a, b) \vee C(a, b))^{\mathcal {S}} = P^{\mathcal {S}}(a, b) \oplus C^{\mathcal {S}}(a, b)\\&\quad =(inf_{c\in U} (C^{\mathcal {S}}(c, a)\Rightarrow _{r}C^{\mathcal {S}}(c, b))) \oplus C^{\mathcal {S}}(a, b) \end{aligned}$$

The definition of fuzzy RCC expressions is intended to enhance the representation ability of fuzzy spatial relationships regarding to the fuzzy spatial concrete domains. Now, fuzzy spatial concrete domains not only represent atomic fuzzy RCC relations, but also complex fuzzy RCC expressions connected with boolean operators.

4.2 Admissibility

Based on fuzzy RCC relations and fuzzy RCC expressions, we give the definitions of the corresponding property, i.e., we need to ensure that the fuzzy spatial concrete domain $\mathcal {S}$ is admissible.

Definition 4

Let $\mathcal {S}=(\Delta _{\mathcal {S}}, \Phi _{\mathcal {S}})$ be a fuzzy spatial concrete domain. An $\mathcal {S}$-conjunction is a finite fuzzy spatial predicate conjunction of the form

$$\begin{aligned} c=\bigwedge _{j=1}^{n}(r_j(x_1^{(j)}, x_2^{(j)})\bowtie k_j) \end{aligned}$$

(1)

where $r_j$ is a binary fuzzy spatial predicate for $j\le n$, the $x_i^{(j)}$ denotes the set of region variables and $\bowtie \in \{\ge , >,\le , <\}$, $k_j\in [0, 1]$. We call an $\mathcal {S}$-conjunction as satisfiable if and only if there exists a mapping function $\delta$ from the spatial region variables to the elements of $\Delta _{\mathcal {S}}$ s.t. $r_j^{\mathcal {S}}(\delta (x_1^{(j)}), \delta (x_2{(j)})\bowtie k_j$ for each $j \le n$. We call such a mapping function $\delta$ as a solution for c. We call $\mathcal {S}$ is admissible iff (i) the collection of fuzzy spatial predicates is closed under negation and contains $\top _{\mathcal {S}}$ for $\Delta _{\mathcal {S}}$, and (ii) the $\mathcal {S}$-conjunctions satisfiability is decidable. Here, we call the $\mathcal {S}$-conjunctions satisfiability problem as $\mathcal {S}$-satisfiability.

Before giving the proof the admissibility of fuzzy spatial concrete domain $\mathcal {S}$, we first give the formal definition of fuzzy RCC network as follows:

Definition 5

(Fuzzy RCC network) Let V and R be countably infinite sets of spatial variables and fuzzy RCC topological relation names (DC, TPP, P, PO, PP, DR, EC, O, EQ, NTP, NTTP) from Table 1, respectively. A fuzzy RCC formula is an expression of the form $r(a, b)\bowtie k$, with $a, b\in V, r\in R, \bowtie \in \{\ge , >, \le , <\}, k\in [0, 1]$. A fuzzy RCC network $\Theta$ is a set of fuzzy RCC formulas. The set of spatial variables used in fuzzy RCC network $\Theta$ is denoted by Var.

For example, a fuzzy RCC network $\Theta =\{C(b,c)\ge 0.7, P(c,a) \ge 0.6, O(a, c) \ge 0.3, NTP(a, b) \ge 0.5\}$.

Lemma 1

Finite fuzzy RCC predicate conjunction’s satisfiability problem is decidable.

Proof

As mentioned by Haarslev et al. (1999), deciding the satisfiability of fuzzy RCC predicate conjunction can be reduced to deciding the consistency of fuzzy RCC network. Thus, we prove the lemma by reducing satisfiability of fuzzy RCC predicate conjunctions to satisfiability of fuzzy RCC network. Let $\Theta$ be a fuzzy RCC network presented in Definition 5. Define a finite conjunction of fuzzy RCC predicates c from $\mathcal {S}$ as follows:

$$\begin{aligned} c=\bigwedge _{j=1}^{n}(r_j(x_1^{(j)}, x_2^{(j)})\bowtie k_j), \end{aligned}$$

where, $r_j$ is a fuzzy RCC relation predicate for $j \le n$, $x_i^{(j)}$ denote the set of region variables $(i =1, 2)$ for $j \le n$, $\bowtie$ $\in \{\ge , >, \le , <\}$ and $k_j \in [0, 1]$.

First, we need a transformation step that translates the conjunction c into a fuzzy RCC network $\Theta$. The set $Var(\Theta )$ of spatial variables is exactly the set of the variables occurring in c, i.e.,

$$\begin{aligned} Var(\Theta ) = \{x_1^1, x_2^1, \ldots , x_1^j, x_2^j,\ldots , x_1^n, x_2^n\}. \end{aligned}$$

Each conjunct $r_j(x_1^j, x_2^j) \bowtie k_j$ from c is a fuzzy RCC formula in $\Theta$. Thus, a fuzzy RCC network $\Theta = \{r_1(x_1^1, x_2^2) \bowtie k_1, \ldots ,r_j(x_1^j, x_2^j) \bowtie k_j, \ldots , r_n(x_1^n, x_2^n) \bowtie k_n\}$.

From (Schockaert et al. 2009), we know that the satisfiability problem of fuzzy RCC network can be decided by a linear programming solver (Karmarkar 1984). Moreover, Schockaert et al. (2009) have proved that this satisfiability problem is NP-complete. Thus, the satisfiability problem of RCC-8 and fuzzy RCC network have the same complexity, i.e., checking the satisfiability problem of fuzzy RCC network is NP-complete. $\square$

Lemma 2

The satisfiability problem of finite fuzzy RCC expression conjunction is decidable.

Proof

Since fuzzy RCC expression is obtained by a Boolean combination of fuzzy RCC relations, the satisfiability problem of finite fuzzy RCC expression conjunction can be reduced to the satisfiability problem of finite fuzzy RCC predicate conjunction. We start with how to translate the finite fuzzy RCC expression conjunction to the finite fuzzy RCC predicate conjunction.

Define a finite conjunction of fuzzy RCC expression $c_r$ from $\mathcal {S}$ as follows:

$$\begin{aligned} c_r =\bigwedge _{j=1}^{n}(\mathbf{r} _j(x_1^{(j)}, x_2^{(j)})\bowtie k_j), \end{aligned}$$

where, $\mathbf{r} _j$ is a fuzzy RCC relation predicate for $j \le n$, $x_i^{(j)}$ denote the set of region variables $(i =1, 2)$ for $j \le n$, $\bowtie$ $\in \{\ge , >, \le , <\}$ and $k_j \in [0, 1]$. We analyze the decidability of the conjunction as follows:

• (i) if $\mathbf{r} _j = \lnot r$ with r is a fuzzy RCC relation, then the conjunct $\mathbf{r} _j(x_1^j, x_2^j) \bowtie k_j$ can be expressed as $r_j(x_1^j, x_2^j)\bowtie ^- k_j^{'}$, where $\bowtie ^-$ denotes the reflections of $\bowtie$ and $k_j^{'} = 1- k_j$. Obviously, by the transformation step of lemma 1, we can obtain a fuzzy RCC network that only contains fuzzy RCC formulas.

• (ii) if $\mathbf{r} _j = r_1\wedge \ldots \wedge r_i$ with $r_i$ is a fuzzy RCC relation, then the conjunct $r_j(x_1^j, x_2^j) \bowtie k_j$ can be expressed as $r_1(x_1^j, x_2^j) \bowtie k_j\wedge \ldots \wedge r_i(x_1^j, x_2^j) \bowtie k_j$. By the transformation step of lemma 1, we can obtain a fuzzy RCC network that only contains fuzzy RCC formulas.

• (iii) if $\mathbf{r} _j = r_1\vee \ldots \vee r_i$ with $r_i$ is a fuzzy RCC relation, then the conjunct $r_j(x_1^j, x_2^j)\bowtie k_j$ can be expressed as $r_1(x_1^j, x_2^j) \bowtie k_j\vee \ldots \vee r_i(x_1^j, x_2^j) \bowtie k_j$ By the transformation step of lemma 1, we can obtain a fuzzy RCC network that contains disjunctions of fuzzy RCC formulas. As mentioned in Schockaert et al. (2009), if a fuzzy RCC network contains disjunctions of fuzzy RCC formulas, a backtracking can be used to determine the satisfiability of the networks.

• (iv) if $\mathbf{r} _j = r_1\rightarrow r_2$ with $r_1$ and $r_2$ are two fuzzy RCC relations, then by the (iii) it follows that the obtained fuzzy RCC network is also decidable because $r_1\rightarrow r_2 \Leftrightarrow r_1\vee r_2$.

Since the lemma 1 has proved that the satisfiability of finite fuzzy RCC predicate conjunction is decidable, the satisfiability of finite fuzzy RCC expression conjunction is also decidable. $\square$

Theorem 1

(Admissible) Fuzzy spatial concrete domain $\mathcal {S}$ is admissible.

Proof

To show that $\mathcal {S}$ is admissible, it needs to be shown that (i) the set of fuzzy spatial predicate names is closed under negation and contains $\top _{\mathcal {S}}$ for $\Delta _{\mathcal {S}}$ and that (ii) the satisfiability of fuzzy spatial predicate conjunction is decidable.

• (i) Fuzzy RCC relations are mutually exclusive and exhaustive. Obviously, the set of fuzzy spatial predicate names is closed under negation and contains $\top _{\mathcal {S}}$ for $\Delta _{\mathcal {S}}$. For any fuzzy spatial predicate $r\in \Phi _{\mathcal {S}}$, there exists a fuzzy spatial predicate $q \in \Phi _{\mathcal {S}}$ such that semantic interpretation $q^{\mathcal {S}} = (\lnot r)^{\mathcal {S}}$. For example, for fuzzy RCC relation predicate $C \in \Phi _{\mathcal {S}}$ , there is a predicate $DC \in \Phi _{\mathcal {S}}$ such that $DC^{\mathcal {S}} = \ominus C = (\lnot C)^{\mathcal {S}}$.

• (2) By Definition 2, we know that fuzzy spatial predicates consist of fuzzy RCC relation predicates and fuzzy RCC expression. Notice that Lemma 1 of this paper has proved that finite fuzzy RCC predicate conjunction’s satisfiability problem is decidable. Lemma 2 of this paper has proved that the satisfiability problem of finite fuzzy RCC expression conjunction is decidable. Thus, the satisfiability of fuzzy spatial predicate conjunction can be decided.

$\square$

As mentioned in Baader and Hanschke (1991), if a concrete domain is admissible, then it can be extended to DL, i.e., the inadmissible concrete domain can lead to undecidable problems of the extended DLs. In the next section, we will extend fuzzy $\mathcal {ALC}$ (Straccia 2001) with our fuzzy spatial concrete domain $\mathcal {S}$.

4.3 Decision approach

Our decision approach is based on the existing reasoning algorithm and results proposed by Schockaert et al. (2009). The detail idea of decision approach consists of two steps. Here, let $\mathcal {H}$ be a set of fuzzy RCC expressions involving variables from a set $V=\{v_1, v_2 \ldots v_n\}$

• (i) Rewriting the fuzzy RCC expressions in $\mathcal {H}$ such that only disjunctions of fuzzy RCC expressions involving C, P, O, and NTP occur, and get a set $\mathcal {H}_s$. The rewriting is based on the rules in Table 1. Here, $\mathcal {H}_s$ is equivalent to $\mathcal {H}$ (Schockaert et al. 2009).

• (ii) Constructing the corresponding system of linear inequalities $\Sigma$ from the set $\mathcal {H}_s$. If $\Sigma$ has a solution, the $\mathcal {H}_s$ is satisfiable, thus obtaining a set $\mathcal {H}$ is also satisfiable. This step includes two cases.

Case 1: If $\Sigma$ does not contain any disjunctions, we can use the well-known lp_solve¹ linear programming solver to decide whether $\Sigma$ has a solution.

Case 2: If $\Sigma$ contains some disjunctions, we can use a backtracking algorithm to determine whether any choice of the disjunct leads to a system of linear inequalities that has a solution.

For example, $\Sigma = \{ C(a, b) \ge 0.5, O(b, a) \le 0.7 \}$. We use the lp_solve to decide that $\Sigma$ has a solution, i.e., $C(a, b) =O(b, a) =$0.6. For the detailed algorithm, we refer the reader to Schockaert et al. (2009) for reasoning algorithm and Karmarkar (1984) for linear programming algorithm.

5 A fuzzy spatial description logic f-${\mathcal {ALC}}({\mathcal S})$

In this section, by extending the well known fuzzy $\mathcal {ALC}$ DL with fuzzy spatial concrete domains $\mathcal {S}$, we propose a fuzzy spatial DL called f-${\mathcal {ALC}}({\mathcal S})$. First of all, we give a formal definition of f-${\mathcal {ALC}}({\mathcal S})$ syntax structure (see Sect. 5.1). Moreover, a semantic interpretation of f-${\mathcal {ALC}}({\mathcal S})$ is provided (see Sect. 5.2). Finally, we define an f-${\mathcal {ALC}}({\mathcal S})$ knowledge base (see Sect. 5.3).

5.1 Syntax structure of f-${\mathcal {ALC}}({\mathcal S})$

The fuzzy spatial description logic f-${\mathcal {ALC}}({\mathcal S})$ is obtained from fuzzy $\mathcal {ALC}$ (Straccia 2001) by adding a fuzzy spatial concrete domain $\mathcal {S}$. The f-${\mathcal {ALC}}({\mathcal S})$ allows to define concepts with reference to fuzzy spatial concrete domain $\mathcal {S}$. Here we will give the formal definition of f-${\mathcal {ALC}}({\mathcal S})$ syntax as follows. We refer here to the syntax of fuzzy ${\mathcal {ALC}}({\mathcal D})$ as defined in Straccia (2009).

Definition 6

(f-${\mathcal {ALC}}({\mathcal S})$ Syntax) Let $N_C, N_R, N_T, N_I$, and $N_O$ be mutually disjoint and countably infinite sets of concept names, abstract roles names, concrete roles names, abstract individuals, and fuzzy spatial regions. Let $R\in N_R$ and $T\in N_T$. Similar to the syntax of fuzzy $\mathcal {ALC}$ (Straccia 2001, 2009), the f-${\mathcal {ALC}}({\mathcal S})$-concepts can be built inductively by the following syntactic rules:

$$\begin{aligned} C, D \rightarrow \top \mid \perp \mid A \mid \lnot C \mid C\sqcap D \mid C\sqcup D \mid \forall R.C \mid \exists R.C \mid \exists (T_1,T_2).\mathbf{r} \mid \forall (T_1,T_2).\mathbf{r} , \end{aligned}$$

where $\top$ denotes a top concept, $\bot$ a bottom concept, $A\in C$ atomic concepts, and $\mathbf{r} \in \Phi _{\mathcal {S}}$ represents a fuzzy RCC expression.

5.2 Semantic interpretation of f-${\mathcal {ALC}}({\mathcal S})$

Based on the Definition 6 and Zadeh logic, we achieve the semantic interpretation of f-${\mathcal {ALC}}({\mathcal S})$. The semantic of f-${\mathcal {ALC}}({\mathcal S})$ is a combination of the semantics for fuzzy $\mathcal {ALC}$ and fuzzy spatial concrete domain $\mathcal {S}$. We refer here to the semantic definition of (Straccia 2009).

Definition 7

(f-${\mathcal {ALC}}({\mathcal S})$ Semantics) Let $\mathcal {S}=(\Delta _{\mathcal {S}}, \Phi _{\mathcal {S}})$ be a fuzzy spatial concrete domain. A fuzzy interpretation $\mathcal {I}$ with respect to $\mathcal {S}$ is a pair $\mathcal {I} = (\Delta ^{\mathcal {I}}, \bullet ^{\mathcal {I}})$, where $\Delta ^{\mathcal {I}}$ is a nonempty set composed of individuals in fuzzy abstract domain, disjoint from $\Delta _{\mathcal {S}}$, and $\bullet ^{\mathcal {I}}$ is a fuzzy interpretation function, which maps:

• each abstract concept name $C \in N_C$ into a function $C^{\mathcal {I}}: \Delta ^{\mathcal {I}} \rightarrow [0, 1]$

• each concrete variable region $x\in N_O$ into an element $x^{\mathcal {I}} \in \Delta _{\mathcal {S}}$ that is x itself, i.e., $x^{\mathcal {I}} = x$

• each abstract role name $R \in N_R$ into a function $R^{\mathcal {I}}: \Delta ^{\mathcal {I}} \times \Delta ^{\mathcal {I}} \rightarrow [0, 1]$

• each concrete role name $T \in N_T$ into a function $T^{\mathcal {I}}: \Delta ^{\mathcal {I}} \times \Delta _{\mathcal {S}} \rightarrow [0, 1]$

• each concrete feature $f \in N_T$ into a function $f^{\mathcal {I}}: \Delta ^{\mathcal {I}} \times \Delta _{\mathcal {S}} \rightarrow \{0, 1\}$. For each individual $a \in N_I$, only one concrete variable region $x \in N_O$ should be allowed to have $f^{\mathcal {I}}(a, x) = 1$

• each fuzzy spatial predicate $r \in \Phi _{\mathcal {S}}$ into a function $r^{\mathcal {S}}: \Delta _{\mathcal {S}} \times \Delta _{\mathcal {S}} \rightarrow [0, 1]$ satisfying the definition of fuzzy RCC relations presented in Table 1 and Definition 3.

For example, if a fuzzy RCC expression $\mathbf{r} = r_1\vee \ldots \vee r_k$, where atomic RCC relations $r_1, \ldots , r_k \in \Phi _{\mathcal {S}}$, then, the fuzzy function $\bullet ^{\mathcal {I}}$ can interpret the fuzzy RCC expression as follows:

$$\begin{aligned} (\mathbf{r} (x, y))^{\mathcal {I}} = (r_1\vee \ldots \vee r_k)^{\mathcal {S}}(x^{\mathcal {I}}, y^{\mathcal {I}}) = r_1^{\mathcal {S}}(x, y) \oplus \ldots \oplus r_k^{\mathcal {S}}(x, y) \end{aligned}$$

The fuzzy interpretation $\bullet ^{\mathcal {I}}$ can be also extended to the semantics of f-${\mathcal {ALC}}({\mathcal S})$ complex concepts as below (where $u, v \in \Delta ^{\mathcal {I}}, x, y \in \Delta _{\mathcal {S}}$):

• $\top ^{\mathcal{I}}(u)=1$

• $\bot ^{\mathcal {I}}(u)=0$

• $(\lnot C)^{\mathcal {I}}(u)=\ominus C^{\mathcal {I}}(u)$

• $(C\sqcap D)^{\mathcal {I}}(u)=C^{\mathcal {I}}(u) \otimes D^{\mathcal {I}}(u)$

• $(C\sqcup D)^{\mathcal {I}}(u)=C^{\mathcal {I}}(u) \oplus D^{\mathcal {I}}(u)$

• $(\forall R.C)^{\mathcal {I}}(u)= inf_{v\in {\Delta ^{\mathcal {I}}}} \{ \ominus R^{\mathcal {I}}(u,v)\oplus C^{\mathcal {I}}(v)\}$

• $(\exists R.C)^{\mathcal {I}}(u)= sup_{v\in {\Delta ^{\mathcal {I}}}} \{ R^{\mathcal {I}}(u,v)\otimes C^{\mathcal {I}}(v)\}$

• $(\forall (T_1,T_2).\mathbf{r} )^{\mathcal {I}}(u)= inf_{x,y\in {\Delta _{\mathcal {S}}}} \{( T_1^{\mathcal {I}}(u,x) \otimes T_2^{\mathcal {I}}(u,y))\Rightarrow \mathbf{r} ^{\mathcal {S}}(x,y)\}$

• $(\exists (T_1,T_2).\mathbf{r} )^{\mathcal {I}}(u)= sup_{x,y\in {\Delta _{\mathcal {S}}}} \{ T_1^{\mathcal {I}}(u,x) \otimes T_2^{\mathcal {I}}(u,y)\otimes \mathbf{r} ^{\mathcal {S}}(x,y)\}$

5.3 Knowledge base of f-${\mathcal {ALC}}({\mathcal S})$

An f-${\mathcal {ALC}}({\mathcal S})$ knowledge base $\mathcal {K} = (\mathcal {T}, \mathcal {A})$ built with our fuzzy DL framework consists of two parts: (i) a fuzzy TBox $\mathcal {T}$, which describes a set of fuzzy axioms for fuzzy abstract domain; (ii) a fuzzy ABox $\mathcal {A}$, which denotes a finite set of fuzzy assertions. We first give the formal definition of these two parts.

Definition 8

(Fuzzy TBox $\mathcal {T}$) A fuzzy TBox $\mathcal {T}$ is a finite set of fuzzy terminology which consists of two forms: (i) fuzzy general concept inclusions (GCIs), which is based on the form $C \sqsubseteq D$, and (ii) fuzzy concept definitions, which is based on the form $C = D$, where C and D are arbitrary fuzzy abstract concepts. From the perspective of semantics,

$\mathcal {I}$ satisfies $C \sqsubseteq D$ iff $\forall a\in \Delta ^{\mathcal {I}}, C^{\mathcal {I}}(a) \le D^{\mathcal {I}}(a)$,

$\mathcal {I}$ satisfies $C = D$ iff $\forall a\in \Delta ^{\mathcal {I}}, C^{\mathcal {I}}(a) = D^{\mathcal {I}}(a)$.

A fuzzy interpretation $\mathcal {I}$ satisfies a fuzzy TBox $\mathcal {T}$ if and only if it satisfies each fuzzy axioms appearing in $\mathcal {T}$; in the condition, we call that $\mathcal {I}$ is a model of $\mathcal {T}$ (denoted $\mathcal {I} \models \mathcal {T}$).

Please note that our definition of fuzzy TBox differs from the one presented by Straccia in the following way. For the formal definition of fuzzy TBox, Straccia defines a fuzzy subsumption of fuzzy concepts. However, we give the formal definition of a crisp subsumption, which is used for describing subsumption by the fuzzy set theory (George J and Bo 1995).

To describe f-${\mathcal {ALC}}({\mathcal S})$, we need to consider two different two types of fuzzy TBox $\mathcal {T}$ which is made of general fuzzy TBoxes and simple fuzzy TBoxes. It should be noted that a general fuzzy TBox is a finite set $\mathcal {T}$ of GCIs. A fuzzy TBox is called simple if it neither includes cyclic nor fuzzy GCIs, where acyclic means that for fuzzy axioms in the forms of $C \sqsubseteq D$ or $C = D$, there is no a concept name C that is defined by itself either directly or indirectly.

An acyclic TBox is a finite set of fuzzy concept definitions which must satisfy one condition: for each fuzzy concept name C, there exists at most one fuzzy concept definition in the form of $C = D$ appearing in $\mathcal {T}$.

A fuzzy concept name C is defined w.r.t an acyclic TBox $\mathcal {T}$ if $\mathcal {T}$ contains a fuzzy concept definition in the form of $C = D$; in the condition, we say that D is definitional of C in $\mathcal {T}$.

Definition 9

(Fuzzy ABox $\mathcal {A}$) A fuzzy ABox $\mathcal {A}$ is a finite collection of fuzzy assertions having four forms: $\langle C(a) \bowtie k \rangle$, $\langle R(a, b) \bowtie k \rangle$, $\langle T(a, x) \bowtie k \rangle$, and $\langle \mathbf{r} (x, y) \bowtie k \rangle$, where, $\bowtie \in \{\ge , >, \le , <\}, k \in [0, 1]$. The fuzzy assertion ABox $\mathcal {A}$ consists of the following four types of assertions:

• A fuzzy concept assertion $\langle C(a) \bowtie k\rangle$, which means that an individual a is an instance of concept C with degree $\bowtie k$.

• A fuzzy abstract role assertion $\langle R(a, b) \bowtie k\rangle$, which means that a pair of individuals (a, b) is an instance of abstract role R with degree $\bowtie k$.

• A fuzzy concrete role assertion $\langle T(a, x) \bowtie k\rangle$, which means that an individual a is related to fuzzy region x via concrete role T with degree $\bowtie k$.

• A fuzzy spatial relation assertion $\langle \mathbf{r} (x, y) \bowtie k\rangle$, which means that a pair of regions (x, y) is an instance of the spatial relation $\mathbf{r}$ with degree $\bowtie k$.

For a fuzzy interpretation $\mathcal {I}$,

• $\mathcal {I}$ satisfies $\langle C(a) \bowtie k\rangle$ if and only if $C^{\mathcal {I}}(a^{\mathcal {I}}) \bowtie k$,

• $\mathcal {I}$ satisfies $\langle R(a, b) \bowtie k\rangle$ if and only if $R^{\mathcal {I}}(a^{\mathcal {I}},b^{\mathcal {I}}) \bowtie k$,

• $\mathcal {I}$ satisfies $\langle T(a, x) \bowtie k\rangle$, if and only if $T^{\mathcal {I}}(a^{\mathcal {I}},x) \bowtie k$,

• $\mathcal {I}$ satisfies $\langle \mathbf{r} (x, y) \bowtie k\rangle$ if and only if $\mathbf{r} ^{\mathcal {S}}(x,y) \bowtie k$.

• $\mathcal {I}$ satisfies a fuzzy ABox $\mathcal {A}$ if and only if it satisfies each fuzzy assertions appearing in $\mathcal {A}$; in the condition, we say that $\mathcal {I}$ is a model of $\mathcal {A}$ (denoted $\mathcal {I} \models \mathcal {A}$).

In conclusion, a fuzzy interpretation $\mathcal {I}$ satisfies an f-${\mathcal {ALC}}({\mathcal S})$ knowledge base $\mathcal {K}$ if and only if it satisfies each fuzzy TBoxs and each fuzzy ABox appearing in $\mathcal {K}$; in the condition, we say that $\mathcal {I}$ is a model of $\mathcal {K}$ (denoted $\mathcal {I}\models \mathcal {K}$).

The reasoning problems can be summarized into three cases as follows:

• (i) f-${\mathcal {ALC}}({\mathcal S})$-concept satisfiability: An f-${\mathcal {ALC}}({\mathcal S})$-concept C w.r.t fuzzy TBox $\mathcal {T}$ is satisfiable (unsatisfiable) iff there exists (does not exist) a fuzzy interpretation $\mathcal {I}$ for which there is some $a\in \Delta ^{\mathcal {I}}$ s.t. $C^{\mathcal {I}}(a) = k$, and $k\in (0, 1]$; in the condition, C is called k-satisfiable.

• (ii) f-${\mathcal {ALC}}({\mathcal S})$ ABox consistency: in f-${\mathcal {ALC}}({\mathcal S})$, fuzzy ABox $\mathcal {A}$ w.r.t fuzzy TBox $\mathcal {T}$ is consistent if and only if there is a model $\mathcal {I}$ for $\mathcal {T}$ that is also a model for $\mathcal {A}$.

• (iii) f-${\mathcal {ALC}}({\mathcal S})$ knowledge base consistency: in f-${\mathcal {ALC}}({\mathcal S})$, a fuzzy knowledge base $\mathcal {K}$ is called satisfiable (unsatisfiable) if and only if it satisfies a condition: there exists (does not exist) a fuzzy interpretation $\mathcal {I}$ which satisfies every fuzzy ABox $\mathcal {A}$ and fuzzy TBox $\mathcal {T}$ appearing in $\mathcal {K}$; in the condition, we call $\mathcal {I}$ is a model of $\mathcal {K}$.

Now, we take an example to illustrate the knowledge representation ability of f-${\mathcal {ALC}}({\mathcal S})$.

Example 1

Suppose that a satellite image $i_1$ represents the snapshot of 1st May at 8:00 a.m. This image describes the situation of a foggy region and a windy region. A foggy region $r_1$ and a windy region $r_2$ have the fuzzy spatial relation “$O\wedge C \ge 0.4$”. It should be noted that the topological relation C is called connection (see Table 1 in Sect. 3.3). Fig. 1 shows the mapping from fuzzy abstract domain to fuzzy spatial concrete domain.

The fuzzy abstract domain in Fig. 1 includes fuzzy spatial concepts Fog, Wind and their individuals fog-a and wind-b. For fuzzy spatial concrete domain, the individuals in the abstract level correspond to different fuzzy spatial region $r_1$ and $r_2$, and their fuzzy topological relations.

Fig. 1

The mapping from fuzzy abstract domain to fuzzy spatial concrete domain

Based on the above description, we consider an f-${\mathcal {ALC}}({\mathcal S})$ knowledge base $\mathcal {K} = (\mathcal {T}, \mathcal {A})$, where

• $\mathcal {T}=\{$ SatelliteMap = Map $\sqcap$ $\exists$ Depicts.Wind $\sqcap$ $\exists$ Depicts.Fog $\sqcap$ $\exists$(has-region, has-region).($O\wedge C$) $\}$,

• $\mathcal {A} = \{\langle$SatelliteMap($i_1$), $\ge ,1\rangle$, $\langle$Wind(wind-b), $\ge ,0.8\rangle$, $\langle$Fog(fog-a), $\ge , 0.9\rangle$, $\langle$Depicts($i_1$, wind-b), $\ge , 0.8\rangle$, $\langle$Depicts($i_1$, fog-a), $\ge , 0.6\rangle$, $\langle$has-region(fog-a, $r_1$), $\ge , 1\rangle$, $\langle$ has-region(wind-b, $r_2$), $\ge , 1\rangle$, $\langle$($O\wedge C$)($r_1$, $r_2$), $\ge$, 0.4$\rangle \}$.

6 Reasoning with f-${\mathcal {ALC}}({\mathcal S})$

In this section, we will show the reasoning of f-${\mathcal {ALC}}({\mathcal S})$ allowing the integration of fuzzy DL reasoning with reasoning about fuzzy spatial regions. First, we provide a tableau-based decision procedure for determining the consistency problem of f-${\mathcal {ALC}}({\mathcal S})$ ABox $\mathcal {A}$ (See Sect. 6.1). Then, we give one example to illustrate how to determine the consistency of f-${\mathcal {ALC}}({\mathcal S})$ ABox $\mathcal {A}$ with our algorithm (See Sect. 6.2). Finally, we prove the correctness and complexity of the decision procedure (See Sect. 6.3).

6.1 A Tableau algorithm for f-${\mathcal {ALC}}({\mathcal S})$

Currently, tableau-based algorithms are the most widely used reasoning technique for description logics. Similarly to fuzzy $\mathcal {ALC}$ (Straccia 2006), deciding fuzzy ABox consistency problem w.r.t. a fuzzy TBox is a basic issue in the process of fuzzy $\mathcal {ALC}$ reasoning, and some inference problems (e.g., knowledge base satisfiability, concept subsumption) can be reduced to ABox consistency problem. Hence, in this paper, we concentrate on the decidable tableau-based algorithm for determining the f-${\mathcal {ALC}}({\mathcal S})$ ABox $\mathcal {A}$ consistency w.r.t. TBoxs.

The basic idea of our tableau algorithm is to try to construct a model of $\mathcal {A}$. If the algorithm succeeds to construct a model, then $\mathcal {A}$ has a model. Otherwise, $\mathcal {A}$ does not have a model. Like various DLs (such as fuzzy $\mathcal {ALC}$ and ${\mathcal {ALC}}({\mathcal D})$), our tableau algorithm also considers a data structure called a completion forest as a model for $\mathcal {A}$. The completion forest model is selected since our proposed fuzzy DL includes a so-called forest model attribute, for example, ABox $\mathcal {A}$ contains many individuals and arbitrary roles can connect two different individuals.

Before constructing the completion forest model, we must transform each concept in $\mathcal {A}$ into equivalent ones in Negation Normal Form (short for NNF). For an arbitrary f-${\mathcal {ALC}}({\mathcal S})$ concept, the feature of its equivalent concept in NNF is the negation on the front of concept name. By using DeMorgan’s laws (Straccia 2001), Łukasiewicz complement, and Kleene-Dienes fuzzy implication operators, all f-${\mathcal {ALC}}({\mathcal S})$ concepts in $\mathcal {A}$ can also be transformed into their equivalent NNF form in a linear time (Straccia 2006). Following Straccia , the detailed transformation rules are shown as follows:

• $\lnot \top =\bot$,

• $\lnot \bot =\top$,

• $\lnot \lnot C=C$,

• $\lnot (C\sqcap D)=\lnot C\sqcup \lnot D$,

• $\lnot (C\sqcup D)=\lnot C\sqcap \lnot D$,

• $\lnot (\forall R.C)=\exists R.\lnot C$,

• $\lnot (\exists R.C)=\forall R.\lnot C$,

• $\lnot (\forall (T_1,T_2).\mathbf{r} )=\exists (T_1,T_2).\lnot \mathbf{r}$,

• $\lnot (\exists (T_1,T_2).\mathbf{r} )=\forall (T_1,T_2).\lnot \mathbf{r}$

All above transformation rules do not change the semantics of concepts due to the syntax structure of f-${\mathcal {ALC}}({\mathcal S})$ defined in Definition 6. In our tableau algorithm, without loss of generality, all f-${\mathcal {ALC}}({\mathcal S})$ concepts in $\mathcal {A}$ are in NNF. Besides, we make an important assumption: f-${\mathcal {ALC}}({\mathcal S})$ TBox $\mathcal {T}=\emptyset$ because the rather weak acyclic TBox can make ABox consistency NEXPTIME-Hard for concrete domain.

In order to decide f-${\mathcal {ALC}}({\mathcal S})$ ABox consistency problem, we need to construct a completion forest through a tableau algorithm. Due to the semantic interpretation of f-${\mathcal {ALC}}({\mathcal S})$, the completion forest we will define includes two kinds of nodes: (i) abstract ones, which represent abstract individuals of fuzzy abstract domain $\Delta ^{\mathcal {I}}$; (ii) concrete ones, which represent concrete variable regions of the concrete domain $\Delta _{\mathcal {S}}$. It should be noted that the following definitions are extensions of several properties described by Straccia (2001).

Definition 10

(Sub-concepts) For an arbitrary fuzzy concept C, the set sub(C) of its sub-concepts can be defined recursively as follows:

• $sub(A) = \{ A \}$: $A \in C$ is an atomic concept

• $sub(\lnot C) = \{ \lnot C \} \cup sub(C)$

• $sub(C\sqcap D) = \{ C\sqcap D \} \cup sub(C) \cup sub(D)$

• $sub(C\sqcup D) = \{ C\sqcup D \} \cup sub(C) \cup sub(D)$

• $sub( \forall R.C) = \{ \forall R.C \} \cup sub(C)$

• $sub( \exists R.C) = \{ \exists R.C \} \cup sub(C)$

• $sub( \exists (T_1,T_2).\mathbf{r} ) = \{ \exists (T_1,T_2).\mathbf{r} \}$

• $sub( \forall (T_1,T_2).\lnot \mathbf{r} ) = \{ \forall (T_1,T_2).\lnot \mathbf{r} \}$

• $sub(C\sqsubseteq D) = sub(C) \cup sub(D)$

• $sub(\mathcal {S}) = \bigcup \limits _{\forall C\in \mathcal {S}} sub(C)$: $\mathcal {S}$ is a set of concepts

Definition 11

(Sub-Expression) For an arbitrary fuzzy RCC expression $\mathbf{r}$, the set $sub(\mathbf{r} )$ of its sub-expression can be defined as follows:

• $sub(\mathbf{r} )=\{ \mathbf{r} \}$: $\mathbf{r} =r(a,b) \mid \lnot \mathbf{r}$

• $sub(\mathbf{r} _1 \vee \ldots \vee \mathbf{r} _n)= sub(\mathbf{r} _1)\cup \ldots \cup sub(\mathbf{r} _n)$

• $sub(\mathbf{r} _1 \wedge \ldots \wedge \mathbf{r} _n)= sub(\mathbf{r} _1)\cup \ldots \cup sub(\mathbf{r} _n)$

• $sub(\mathbf{r} _1 \rightarrow \mathbf{r} _2)= sub(\lnot \mathbf{r} _1)\cup sub(\mathbf{r} _2)$

Now, we define the representation of completion forest.

Definition 12

(Completion forest) Given an f-${\mathcal {ALC}}({\mathcal S})$ ABox $\mathcal {A}$. Let $O_a$ and $O_c$ be disjoint and countably infinite sets of fuzzy abstract nodes and fuzzy concrete nodes, respectively. A completion forest $\mathcal {F}$ can be defined as: $\mathcal {F}= (V_a, V_o, E, L, C_F)$ , where:

• $V_a \subseteq O_a$ is a finite collection of fuzzy abstract nodes,

• $V_o \subseteq O_c$ is a finite collection of fuzzy concrete nodes,

• $E \subseteq (V_a \times (V_a \cup V_o))$ is a collection of edges,

• L is a collection of labels of nodes and edges, which includes three cases:

  • (i) for $a \in V_a$, each abstract node $V_a$ is labelled with a set L(a) of fuzzy concepts C, and L(a) is a tuple $L(a) = (C, \bowtie , k)$, where $C \in sub(\mathcal {A})$ is a fuzzy concept of ABox $\mathcal {A} , k\in (0, 1]$ denotes the membership degree of an instance a to an abstract concept C.

  • (ii) for $a, b \in V_a$, each edge $\langle a, b\rangle \in Ea$ is labelled with a set $L(\langle a, b\rangle )$ of roles R, and $L(\langle a, b\rangle )$ can be represented as a tuple $L(\langle a, b\rangle ) = (R, \bowtie , k)$, where R is a role name; $k \in (0, 1]$ represents the degree of membership of an edge $\langle a, b\rangle$ to a role R.

  • (iii) for $a \in Va$, $x \in Vo$, each edge $\langle a, x\rangle \in Eo$ is labelled with a set $L(\langle a, x\rangle )$ of concrete role T, and $L(\langle a, x\rangle )$ can be defined as a tuple $L(\langle a, x\rangle ) = (T, \bowtie , k)$, where T is a concrete role name; $k \in (0, 1]$ represents the degree of membership of a concrete edge $\langle a, x\rangle$ to a concrete role T.

• $C_F$ is a set of fuzzy spatial relation assertion constraints over $\mathcal {S}$ having a form of fuzzy RCC formulas $\mathbf{r} (x, y)\bowtie k$, where $x, y \in Vo$, $\mathbf{r} \in sub(A), k \in (0, 1]$

If $\langle a, b\rangle$ is an edge with $(R, \bowtie , k)$ occurring in $L(\langle a, b\rangle )$, the node b then is called a $R_{\bowtie ,k}$-successor of a. If $\langle a, x\rangle$ is an edge with $(T, \bowtie , k)$ occurring in $L(\langle a, x\rangle )$, the node x then is called a $T_{\bowtie ,k}$-successor of a.

Next, we initialize the defined completion forest $\mathcal {F}$.

By using an algorithm called Init($\mathcal {A}$), we can initialize a completion forest $\mathcal {F}$ from a given f-${\mathcal {ALC}}({\mathcal S})$ ABox $\mathcal {A}$. In this algorithm, the input is an f-${\mathcal {ALC}}({\mathcal S})$ ABox $\mathcal {A}$ and the output is an initialized completion forest $\mathcal {F}= (V_a, V_o, E, L, C_F)$. The detailed algorithm is shown in Algorithm 1.

We now use the tableau expansion rules to expand the initial completion forest $\mathcal {F}_0$. The tableau expansion rules decompose all concepts in node labels in the syntactical level. As a result, some new nodes are added and some node labels are extended.

Before giving the detailed expansion rules, we first recall one concept: conjugated pairs of fuzzy assertions. This notion mainly describes pairs of fuzzy assertions which can yield a contradiction. If $\theta$ denotes a fuzzy assertion of f-${\mathcal {ALC}}({\mathcal S})$, then $\theta ^c$ denotes the corresponding conjugation of $\theta$. In our proposed f-${\mathcal {ALC}}({\mathcal S})$, there exist four possible conjugated pairs:

• 1. $\{\langle \theta> k_1\rangle , \langle \theta \le k_2\rangle , k_1 > k_2 \}$,

• 2. $\{\langle \theta \ge k_1\rangle , \langle \theta \le m\rangle , k_1 > k_2\}$,

• 3. $\{\langle \theta > k_1\rangle , \langle \theta < k_2\rangle , k_1 \ge k_2\}$,

• 4. $\{\langle \theta \ge k_1\rangle , \langle \theta < k_2\rangle , k_1 \ge k_2 \}$.

As an example, if $\theta$ = $\langle R(a, b) \ge 0.4\rangle$, then $\theta ^c$ may be $\langle R(a, b) < 0.3\rangle$.

Table 2 The tableau expansion rules

As shown in Table 2, we give 16 tableau expansion rules. Here, some technical terminologies are introduced. Let C and D be fuzzy concept terms, a and b fuzzy abstract individual names from C and D, R a fuzzy abstract role term, $T_1$ and $T_2$ fuzzy concrete role terms, $o_1$ and $o_1$ concrete variable region names, x an abstract node, and let r be a fuzzy spatial predicate name from fuzzy spatial concrete domain $\mathcal {S}$. Due to the limitations on the length of this paper, we only show fuzzy assertions involving the inequalities “$\ge$” and “$\le$”. For the inequalities “>” and “<”, the method is the same as the inequalities “$\ge$” and “$\le$”. Here, we do not elaborate them in detail.

Now, following Straccia , we give a formalized notion of contradictory.

Definition 13

(Clash) Suppose that $\mathcal {F}$ is a completion forest, x an abstract node of $\mathcal {F}$, L(x) a label of x. $\mathcal {F}$ contains a clash iff one of the following described conditions hold at least:

• (i) L(x) contains two conjugated triples as described above;

• (ii) L(x) contains a fuzzy axiom $\langle C, <, 0\rangle$;

• (iii) L(x) contains a fuzzy axiom $\langle C, >, k\rangle$ with $k >1$.

If the forest $\mathcal {F}$ does not contain a clash, we then call $\mathcal {F}$ is clash-free.

Definition 14

Suppose that $\mathcal {F}$ is a completion forest. $\mathcal {F}$ is called complete if and only if none of the tableau expansion rules shown in Table 2 is applicable to $\mathcal {F}$. Otherwise, we call $\mathcal {F}$ is incomplete.

Definition 15

With a set of fuzzy spatial relation assertion constraints $C_{\mathcal {F}}$, we associate a fuzzy spatial predicate conjunction

$$\begin{aligned} c=\bigwedge _{j=1}^{n}(r_j(x_1^{(j)}, x_2^{(j)})\bowtie k_j), \end{aligned}$$

$C_{\mathcal {F}}$ is considered as concrete domain satisfiable if and only if c is satisfiable.

According to Theorem 1, we know that our proposed fuzzy spatial concrete domain $\mathcal {S}$ is admissible and $\mathcal {S}$-satisfiability problem is in NP-complete. Thus, the satisfiability problem of c is decidable.

Until now, the 16 tableau expansion rules are given and the clash of completion forest $\mathcal {F}$ is also defined. Next, we describe the tableau-based algorithm to determine whether f-${\mathcal {ALC}}({\mathcal S})$ ABox $\mathcal {A}$ is satisfiable or not. Given an f-${\mathcal {ALC}}({\mathcal S})$ ABox $\mathcal {A}$, the satisfiability problem can be decided through a tableau-based algorithm Con-dec($\mathcal {A}$) as shown in Algorithm 2. This algorithm starts with the initial completion $\mathcal {F}_0$ as an input and takes a boolean value as an output.

As we can see, the above algorithm Con-dec($\mathcal {A}$) describes the procedure of deciding the consistency problem of the input f-${\mathcal {ALC}}({\mathcal S})$ ABox $\mathcal {A}$. The argument of Con-dec is a fuzzy ABox $\mathcal {A}$. The algorithm uses Init($\mathcal {A}$) to initialize a completion forest $\mathcal {F}$. Then, the tableau expansion rules are utilized to expand $\mathcal {F}$ until no more expansion rule can be further utilized to $\mathcal {F}$. If the forest $\mathcal {F}$ contains a clash, the $\mathcal {A}$ is then inconsistent. If $\mathcal {F}$ is clash-free, then the algorithm starts checking whether all fuzzy spatial relation axioms of the form $\langle \mathbf{r} (x, y)\bowtie k\rangle$ in $C_{\mathcal {F}}$ is satisfiable or not. If $C_{\mathcal {F}}$ is not a concrete domain satisfiable, then $\mathcal {A}$ is inconsistent. For the detailed decision approach, we refer the reader to Sect. 4.3. Please note that the Con-dec checks contradictions and fuzzy spatial concrete domain satisfiability separately. This idea of our decision procedure is similar to the tableau algorithm used by Lutz (1999).

Besides, the algorithm Con-dec($\mathcal {A}$) can be used to decide the satisfiability of fuzzy spatial concept C. The satisfiability of fuzzy spatial concept C can also be reduced to determine the consistency problem of fuzzy ABox $\mathcal {A}$ of the form $\{(x, C) > 0\}$. In the next section, we will give one example to illustrate how to decide f-${\mathcal {ALC}}({\mathcal S})$ ABox consistency checking problem with respect to $\mathcal {T}= \emptyset$ with our proposed tableau algorithm.

Compared with the tableau-based reasoning algorithm in (Straccia 2001, 2009), our tableau algorithm includes some different new expansion rules. As shown in Table 2, the rules $\exists \mathbf{r} \ge$, $\exists \mathbf{r} \le$, $\forall \mathbf{r} \ge$, and $\forall \mathbf{r} \le$ are the new expansion rules. Other extension rules are common parts to fuzzy ${\mathcal {ALC}}({\mathcal D})$ (Straccia 2009) and fuzzy $\mathcal {ALC}$ (Straccia 2001).

6.2 Example

In this section, we provide one example of determining f-${\mathcal {ALC}}({\mathcal S})$ ABox consistency problem w.r.t an empty TBox $\mathcal {T}$ with our tableau algorithm to enable readers to understand well the procedure presented in Sect. 6.1. Similar to the example 1, we also consider the example of satellite images.

Example 2

Consider an f-${\mathcal {ALC}}({\mathcal S})$ ABox $\mathcal {A}$ =$\{\langle i$: Image, $\ge$, 1$\rangle$, $\langle s$: SatelliteImage, $\ge$, 1$\rangle$, $\langle (s, i)$: is-a, $\ge$, 1$\rangle$,$\langle a$: Fog, $\ge$, 0.9$\rangle$, $\langle b$: Wind, $\ge$, 0.85$\rangle$, $\langle (s, a)$depicts, $\ge$, 0.7$\rangle \}$.

We expect to determine the consistency of the f-${\mathcal {ALC}}({\mathcal S})$ ABox $\mathcal {A}_1$ = $\mathcal {A} \sqcup \{\langle s$: depicts.Fog $\cap$ depicts.Wind $\cap$ (has-FoggyRegion, has-WindyRegion).$(O\wedge C)$, $\le$, 0.75$\rangle \}$ w.r.t an empty TBox $\mathcal {T}$. According to the algorithm Init($\mathcal {A}$) shown in Algorithm 1, we first initialize a completion forest $\mathcal {F}$ which has four fuzzy abstract nodes $x_a, x_b, x_s$ and $x_i$, then $\mathcal {F}$ contains the following triples:

• $L(x_i)$ = $\{\langle$Image, $\ge$, 1$\rangle \}$,

• $L(x_a)$ = $\{\langle$Fog, $\ge$, 0. 9$\rangle \}$,

• $L(x_b)$ = $\{\langle$Wind, $\ge$, 0.85$\rangle \}$,

• $L(x_s)$ =$\{\langle$SatelliteImage, $\ge$, 1$\rangle$, $\langle$depicts.Fog $\cap$ depicts.Wind $\cap$ (has-FoggyRegion, has-WindyRegion).$(O\wedge C)$, $\le$, 0.75$\rangle \}$,

• $L(\langle x_s, x_i\rangle )$ = $\langle$ is-a, $\ge$, 1$\rangle$,

• $L(\langle x _s, x_a\rangle )$ = $\langle$depicts, $\ge$, 0.8$\rangle$,

• $C_{\mathcal {F}}$ = $\{\emptyset \}$.

Subsequently, by applying these expansion rules shown in Table 2 to each node repeatedly, we have the following steps:

• (1) Apply the $\cap \le$ rule to node $x_s$, then we have $L(x_s) = \{\langle$SatelliteImage, $\ge , 1\rangle \} \cup \{C'\}$, where $C'\in \{\langle$depicts.Fog, $\le , 0.75\rangle , \langle$depicts.Wind $\le , 0.75\rangle$,(has-FoggyRegion, has-WindyRegion).$(O\wedge C)$, $\le , 0.75\rangle \}$

  At this point, we get three possible forests. For the first one $\mathcal {F}_1$, we have $L(x_s)$ =$\{\langle$SatelliteImage, $\ge , 1\rangle , \langle$depicts.Fog, $\le , 0.75\rangle \}$. For the second one $\mathcal {F}_2$, we have $L(x_s)$ =$\{\langle$SatelliteImage, $\ge , 1\rangle , \langle$depicts.Wind, $\le , 0.75\rangle \}$. For the third one $\mathcal {F}_3$, we have $L(x_s)$ =$\{\langle$SatelliteImage,$\ge , 1\rangle , \langle$(has-FoggyRegion, has-WindyRegion).$(O\wedge C)$, $\le , 0.75\rangle \}$.

• (2) Apply the $\exists \le$ rule to $\mathcal {F}_1$, then we have $L(x_a)$ =$\{\langle$Fog, $\ge , 0.9\rangle , \langle$Fog, $\le , 0.75\rangle \}$, and then delete $\langle \exists$ depicts.Fog, $\le , 0.75\rangle$ from $L(x_s)$.

  Obviously, there are two conjugated triples in $L(x_a)$. That is, $\mathcal {F}_1$ contains a clash. Thus, $\mathcal {F}_1$ is unsatisfiable.

• (3) Apply the $\exists \le$ rule to $\mathcal {F}_2$, then we have $L(x_a)$ =$\{\langle$Wind, $\ge , 0.85\rangle , \langle$Wind, $\le , 0.75\rangle \}$, $L(\langle x_a,x_b\rangle )$ = $\varphi ^c$, where $\varphi$ = $\langle$depicts, $\le , 0.75\rangle$, and then delete $\langle \exists$depicts.Fog, $\le , 0.75\rangle$ from $L(x_s)$.

  Obviously, there are two conjugated triples in $L(x_a)$. Since $\mathcal {F}_2$ contains a clash, $\mathcal {F}_2$ is unsatisfiable.

• (4) Apply the $\forall \mathbf{r} \le$ rule to $\mathcal {F}_3$, then create two fuzzy spatial object nodes $\langle o_1, o_2\rangle$ which are $\langle$has-FoggyRegion, has-WindyRegion$\rangle$-successor of $x_s$, such that:

  $$\begin{aligned}&L(\langle x_s, o_1\rangle ) = \{\langle \hbox {has-FoggyRegion}, \ge , 0.25\rangle \},\\&L(\langle x_s, o_2\rangle ) = \{\langle \hbox {has-WindyRegion}, \ge , 0.25\rangle \},\\&C_{\mathcal {F}} = \{\langle (o_1, o_2):(O\wedge C), \le , 0.75\rangle \}, \end{aligned}$$

  and then delete $\langle \forall$(has-FoggyRegion, has-WindyRegion).$(O\wedge C), \le , 0.75\rangle$ from $L(x_s)$.

At this point, no expansion rules can be applied on $\mathcal {F}_3$ and $\mathcal {F}_3$ becomes a completion forest. Then, we start to check the satisfiability of $C_{\mathcal {F}}$. According to the Definitions 2 and 3, $C_{\mathcal {F}}$ can be decomposed into $C_{\mathcal {F}}$ = $\{\langle (o_1, o_2): O, \le , 0.75\rangle \wedge \langle (o_1, o_2): C, \le , 0.75\rangle \}$. Based on the decision approach in Sect. 4.3, it is not hard to see that $C_{\mathcal {F}}$ is satisfiable. Thus, $\mathcal {F}_3$ does not contain a clash. It follows that $\mathcal {A}_1$ is consistent.

The example 2 shows that using our tableau algorithm can solve f-${\mathcal {ALC}}({\mathcal S})$ ABox $\mathcal {A}$ consistency checking problem w.r.t an empty TBox $\mathcal {T}$. As mentioned in Sect. 3.2, some other inference tasks (e.g., concept subsumption, concept satisfiability) can also be transformed into consistency checking of ABox. More precisely, checking satisfiability of a fuzzy spatial concept C of f-${\mathcal {ALC}}({\mathcal S})$ can be transformed into determining the consistency problem of fuzzy ABox $\mathcal {A}$ = $\{(x, C) > 0\}$, where x is an abstract individual of concept C.

6.3 Correctness and complexity

In this section, the correctness and complexity of the tableau algorithm proposed in Sect. 6.1 are proved in detail. The correctness mainly consists of three parts: termination, soundness, and completeness. We prove these on the basis of the correctness proof of the tableau algorithm in the crisp ${\mathcal {ALC}}({\mathcal D})$ proposed by Lutz (2002a) and fuzzy $\mathcal {ALC}$ proposed by Straccia (2001).

Theorem 2

(Termination) Let $\mathcal {A}$ be f-${\mathcal {ALC}}({\mathcal S})$ ABox. For each $\mathcal {A}$ as the input of the tableau algorithm, the algorithm always terminates.

Proof

Let $\mathbf{n} = |sub(\mathcal {A})|$ be the length of fuzzy assertions occurring in $\mathcal {A}$, $\mathbf{d}$ the number of different membership degrees occurring in $\mathcal {A}$, $\mathcal {F}$ a completion forest established by the tableau algorithm, s the maximum of fuzzy RCC predicates occurring in $\mathcal {A}$. Assume that $R_a$ is a collection of fuzzy abstract roles appearing in $\mathcal {A}$, $R_c$ a collection of fuzzy concrete roles appearing in $\mathcal {A}$, $\mathbf{m} = |R_a|$ the number of abstract roles appearing in $\mathcal {A}$, $\mathbf{c} = |R_c|$ the number of abstract roles appearing in $\mathcal {A}$, The termination of the tableau algorithm implies that the applications of the expansion rules are bounded. In other words, there exists an upper that is bound for the completion forest’s size. Once this bound is established, the termination of the algorithm can be proved. For the forest, there are upper bounds for the out-degree and the depth. Thus, it is needed to establish one bound for the out-degree of the forest and one bound for the depth. Obviously, the two bounds are results of expansion rules’ properties. In the following, we first prove the two bounds.

(i) establishing one bound on the out-degree of $\mathcal {F}$.

• The $\exists \ge$ and $\forall \le$ rules only generate some new abstract nodes. Assume that $x \in V_a$ is an element of abstract nodes. More precisely, for each $\langle \exists R.C, \ge , k\rangle \in sub(\mathcal {A})$, the expansion rule $\exists \ge$ rule yields at most one abstract successor of x. For each concept of the form $\langle \forall R.C, \le , k\rangle \in sub(\mathcal {A})$, the expansion $\forall \le$ rule yields at most one abstract successor of x. Since $sub(\mathcal {A})$ contains n $\langle \exists R.C, \ge , k\rangle \in sub(\mathcal {A})$ at most or n $\langle \forall R.C, \le , k\rangle \in sub(\mathcal {A})$ at most, it follows that the upper bound of the abstract successors of x is bounded by $\mathbf{n}$. It is easy to prove that the out-degree of this forest constructed by our proposed method is bounded by $\mathbf{nd}$.

• The $\exists \mathbf{r} \ge$ and $\forall \mathbf{r} \le$ rules only generate some new concrete domain nodes. Assume that $x \in V_a$ is an element of abstract nodes, $o \in V_o$ is an element of concrete domain nodes. More precisely, for each $\langle \exists (T_1, T_2).\mathbf{r} , \ge , k\rangle \in sub(\mathcal {A})$, the $\exists \mathbf{r} \ge$ rule generates at most two concrete successors of x. For each $\langle \forall (T_1, T_2).\mathbf{r} , \le , k\rangle \in sub(\mathcal {A})$ ,the $\forall \mathbf{r} \le$ rule yields at most two concrete successors of x. Since the yielded object nodes can only appear in the leaf nodes of the completion forest and $sub(\mathcal {A})$ contains at most n $\langle \exists (T_1, T_2).\mathbf{r} , \ge , k\rangle \in sub(\mathcal {A})$ or $\langle \forall (T_1, T_2).\mathbf{r} , \le , k\rangle \in sub(\mathcal {A})$, the upper bound of the concrete successors of x is 2n. Obviously, the out-degree of the generated forest is bounded by 2nd.

Thus, the out-degree of the forest generated by our proposed method is bounded by 2nd.

(ii) establishing one bound on the depth of $\mathcal {F}$.

The $\lnot \ge$, $\lnot \le$, $\cap \ge$, $\cap \le$, $\cup \ge$, $\cup \le$, $\exists \ge$ and $\forall \ge$ rules only add fuzzy concept assertion $\langle C, \bowtie , k\rangle$ to node label L(x). For all abstract nodes x in $\mathcal {F}$, we obviously have the depth of the node labels L(x) is bounded by m+c.

• The $\exists \mathbf{r} \le$ and $\forall \mathbf{r} \ge$ rules neither add any new node nor do they change node labels sets information. Thus, these rules are trivial for the depth of the forest.

• The $\exists \ge$ and $\forall \le$ rules only add fuzzy abstract role assertions $\langle (a, b):R \bowtie k\rangle$ to abstract edge label $L(\langle x, y\rangle )$. For all abstract edges $\langle x, y\rangle$ in $\mathcal {F}$, we obviously have the depth of the abstract edge labels $L(\langle x, y\rangle )$ is at most $|R_a| = \mathbf{m}$.

• The $\exists \mathbf{r} \ge$ and $\forall \mathbf{r} \le$ rules do not change abstract node labels but add two concrete domain nodes to $\mathcal {F}$. Moreover, they also add fuzzy concrete role assertions $\langle (a, o):T \bowtie k\rangle$ to concrete edge label $L(\langle x, o\rangle )$. For all concrete edges $\langle x, o\rangle$ in $\mathcal {F}$, we obviously have the depth of the concrete edge labels $L(\langle x, o\rangle )$ is at most $|R_c| = \mathbf{c}$.

Summing up, the depth of $\mathcal {F}$ is bounded by m+c.

We now prove the upper bound of applications of the expansion rules.

Assume that k is the number of nodes. By (i) and (ii), we can obviously obtain that k = (2nd)m+c. Based on the properties of the expansion rules, we analyze the upper bound on applications of the rules as follows:

• For the $\lnot \ge$, $\lnot \le$, $\cap \ge$, $\cap \le$, $\cup \ge$, $\cup \le$, $\exists \ge$ and $\forall \ge$ rules, we can observe that each rule only adds one fuzzy concept assertion to an abstract node label. Moreover, according to these rules, we obtain two features: there are no fuzzy concepts assertions that are removed from node labels and there are no abstract nodes that are removed from F. Since each abstract node label’s size is bounded by n, these rules may be used nk times at most.

• For the $\exists \mathbf{r} \le$, $\exists \mathbf{r} \ge$, $\forall \mathbf{r} \le$ and $\forall \mathbf{r} \ge$ rules, we can observe that each rule adds fuzzy spatial predicate assertions $\langle \mathbf{r} (o_1, o_2) \bowtie k\rangle$ to a constraint $C_{\mathcal {F}}$. Moreover, fuzzy spatial predicate assertions are never removed from the constraints $C_{\mathcal {F}}$. Since the upper bound of concrete domain nodes is k and the upper bound of fuzzy spatial predicates in $\mathcal {A}$ is s, there may be at most $\mathbf{nk} ^\mathbf{s}$ applications of these rules.

• For the $\exists \ge$ and $\forall \le$ rules, we can observe that each rule adds a fuzzy concept assertion $\langle C, \ge , k\rangle$ or $\langle C, \le , k\rangle$ to an abstract label and each rule can be applied once for each $\langle \exists R.C, \ge , k\rangle$ or $\langle \forall R.C, \le , k\rangle$ of any abstract label. Because each abstract node produces one incoming edge, these rules may be applied at most k times.

Summing up, we can conclude that the upper bound of applications of the expansion rules is nk + $\mathbf{nk} ^\mathbf{s}$ +k with k = (2nd)$^\mathbf{m +\mathbf{c} }$. $\square$

We now show the soundness and completeness of our proposed algorithm.

Theorem 3

(Soundness) Suppose that $\mathcal {A}$ is an input f-${\mathcal {ALC}}({\mathcal S})$ ABox to the tableau algorithm. If the algorithm returns consistent, $\mathcal {A}$ then is consistent.

Proof

When started on an input f-${\mathcal {ALC}}({\mathcal S})$ ABox $\mathcal {A}$, if the algorithm returns consistent, there then is a complete and clash-free completion forest $\mathcal {F}$ for $\mathcal {A}$. To prove that $\mathcal {A}$ is consistent, we need to prove that there is a model $\mathcal {I}$ of $\mathcal {A}$. Obviously, this implies that we need to define a fuzzy interpretation $\mathcal {I}$ of $\mathcal {A}$ by using $\mathcal {F}$.

Assume that $\mathcal {F}=(V_a, V_o, E, L, C_{\mathcal {F}})$ is the obtained completion forest from $\mathcal {A}$ . We define a fuzzy interpretation $\mathcal {I} = (\Delta ^{\mathcal {I}}, \Delta _{\mathcal {S}}, \bullet ^{\mathcal {I}})$ of $\mathcal {A}$ by setting $\Delta ^{\mathcal {I}}$ and $\Delta _{\mathcal {S}}$ to the abstract and concrete nodes in $\mathcal {F}$ as follows:

• $\top ^{\mathcal {I}}(a)=1$ for each $a\in V_a$

• $\bot ^{\mathcal {I}}(a)=0$ for each $a\in V_a$

• $\Delta ^{\mathcal {I}} = \{a \mid a \in V_a\}$

• $\Delta _{\mathcal {S}} = \{o \mid o \in V_o\}$

• $C^{\mathcal {I}}(a) = \{ \mu _{a:C} \in [0, 1] \mid a \in V_a \}$ for each $C \in N_C$

• $R^{\mathcal {I}}(a,b) = \{ \mu _{(a,b):R} \in [0, 1] \mid (a,b) \in E \}$ for each $R \in N_R$

• $T^{\mathcal {I}}(a,o) = \{ \mu _{(a,o):T} \in [0, 1] \mid (a,o) \in E \}$ for each $T \in N_T$

• $\mathbf{r} ^{\mathcal {I}}(o_1,o_2) = \{ \mu _{(o_1,o_2):\mathbf{r} } \in [0, 1] \mid (o_1,o_2) \in V_O\times V_O, \mathbf{r} (o_1,o_2)\in C_{\mathcal {F}} \}$

• $a^{\mathcal {I}} = a$ for each $a \in Va$

• $o^{\mathcal {I}} = o$ for each $o \in Vo$

where $\mu _{a:C}, \mu _{(a,b):R}, \mu _{(a,o):T}$, and $\mu _{(o_1,o_2):\mathbf{r} }$ denote binary fuzzy relations.

As described in the Definition 9, a fuzzy interpretation $\mathcal {I}$ is a model of $\mathcal {A}$ implies that it satisfies every fuzzy assertion in $\mathcal {A}$. Thus, in order to prove that a fuzzy interpretation $\mathcal {I}$ is a model of $\mathcal {A}$, we must show that the $\mathcal {I}$ satisfies each fuzzy assertions appearing in $\mathcal {A}$. Here, we use structural induction on concept C: for all $a \in Va, L(a) = (C, \bowtie , k)$ implies $C^{\mathcal {I}}(a) \bowtie k$. Since the expansion rules $\lnot \ge$, $\lnot \le$, $\cap \ge$, $\cap \le$, $\cup \ge$, $\cup \le$, $\exists \ge$, $\exists \le$, $\forall \ge$, $\forall \le$ are the common parts to fuzzy $\mathcal {ALC}$ in our reasoning algorithm, we refer the reader to Straccia (2001) with the proof. In the following, we only show the rest cases of fuzzy assertions.

• Case L(a) = $\langle \exists (T_1,T_2).\mathbf{r} , \ge , k\rangle$. Since the expansion rule “$\exists \mathbf{r} \ge$” is not available, there exists a $\langle T_1, T_2\rangle$-successor $\langle o_1, o_2\rangle$ of a s.t. a set of labels $L(<a, o_1>)$ = $\{<T_1, \ge , k>\}, L(\langle a, o_2\rangle ) = \{\langle T_2, \ge , k\rangle \}$ and $\langle \mathbf{r} (o_1, o_2), \ge , k\rangle \in C_{\mathcal {F}(x)}$. By the definition of $T^{\mathcal {I}}$ and $\mathbf{r} ^{\mathcal {S}}$, we obtain $T_1^{\mathcal {I}}(a, o_1) \ge k$, $T_2^{\mathcal {I}}(a, o_2) \ge k$, and $\mathbf{r} ^{\mathcal {S}}(o_1, o_2) \ge k$. By the inductioin, we obtain $(\exists (T_1,T_2).\mathbf{r} )^{\mathcal {I}}(a) = sup_{o_1,o_2\in \Delta _{\mathcal {S}}}\{ ( T_1^{\mathcal {I}}(a, o_1) \otimes T_2^{\mathcal {I}}(a, o_2) \otimes \mathbf{r} ^{\mathcal {S}}(o_1, o_2)) \}\ge k$. The case for $L(a) = \langle \exists (T_1,T_2).\mathbf{r} , \le , k\rangle$ is similar.

• Case L(a) = $\langle \forall (T_1,T_2).\mathbf{r} , \ge , k\rangle$. Since the expansion rule “$\forall \mathbf{r} \ge$” is not available, there exists a $\langle T_1, T_2\rangle$-successor $\langle o_1, o_2\rangle$ of a such that $L(<a, o_1>)=\varphi _1^c$ with $\varphi _1 = \langle T_1, \le , 1-k\rangle$, $L(<a, o_2>)=\varphi _2^c$ with $\varphi _2 = \langle T_2, \le , 1-k\rangle$. By the definition of $\mathcal {I}$, we obtain $T_1^{\mathcal {I}}(a, o_1) \ge k$, $T_2^{\mathcal {I}}(a, o_2) \ge k$, and $\mathbf{r} ^{\mathcal {S}}(o_1, o_2) \ge k$. By the induction, we obtain $(\forall (T_1,T_2).\mathbf{r} )^{\mathcal {I}}(a) = inf_{o_1,o_2\in \Delta _{\mathcal {S}}}\{ ( T_1^{\mathcal {I}}(a, o_1) \otimes T_2^{\mathcal {I}}(a, o_2)) \rightarrow \mathbf{r} ^{\mathcal {S}}(o_1, o_2) \} \ge k$. The case for $L(a) = \langle \forall (T_1,T_2).\mathbf{r} , \le , k\rangle$ is similar.

Obviously, the fuzzy interpretation $\mathcal {I}$ satisfies every fuzzy assertion in $\mathcal {A}$. Hence, it is easily seen that the fuzzy interpretation $\mathcal {I}$ is a model of $\mathcal {A}$. $\square$

Theorem 4

(Completeness) Suppose that $\mathcal {A}$ is an input f-${\mathcal {ALC}}({\mathcal S})$ ABox to the tableau algorithm. If $\mathcal {A}$ is consistent, the tableau algorithm then returns consistent.

Proof

Since $\mathcal {A}$ is consistent and $\mathcal {A}$ is an input f-${\mathcal {ALC}}({\mathcal S})$ ABox to the tableau algorithm, there exists a fuzzy interpretation $\mathcal {I}$ which must satisfy a condition: the interpretation is a model of $\mathcal {A}$. Let $\mathcal {I} = (\Delta ^{\mathcal {I}}, \Delta _{\mathcal {S}}, \bullet ^{\mathcal {I}})$. To show that the tableau algorithm returns consistent, we need to show that using $\mathcal {I}$ can construct a completion forest which is clash-free and complete. That is to say, by using $\mathcal {I}$, we trigger the applications of expansion rules shown in Table 2 s.t they generate a clash-free and complete completion forest.

Suppose that $\mathcal {F}=(V_a, V_o, E, L, C_{\mathcal {F}})$ is a constructed completion forest from $\mathcal {I}$.

First, we define two mappings as follows:

• $\alpha : V_a \rightarrow \Delta ^{\mathcal {I}}$ is a mapping from abstract nodes of $\mathcal {F}$ into elements of fuzzy abstract domain of $\mathcal {I}$.

• $\beta : V_c \rightarrow \Delta _{\mathcal {S}}$ is a mapping from concrete nodes of $\mathcal {F}$ into elements of fuzzy spatial concrete domains.

• $\mathcal {F}$ is complete iff the two mappings satisfy the following five conditions:

  (i):

  if $\langle \lnot C, \bowtie , k\rangle \in L(a)$, then $\langle \alpha (a), \bowtie ^-, 1-k\rangle \in C^{\mathcal {I}}$, where $\bowtie ^-$ denotes the reflection of $\bowtie.$

  (ii):

  if $\langle C, \bowtie , k\rangle \in L(a),$ then $\langle \alpha (a), \bowtie , k\rangle \in C^{\mathcal {I}}.$

  (iii):

  if b is an R-successor of a, then $\langle (\alpha (a),\alpha (b)), \bowtie , k\rangle \in R^{\mathcal {I}}.$

  (iv):

  if a is an T-successor of o, then $\langle (\alpha (a),\beta (o)), \bowtie , k\rangle \in T^{\mathcal {I}}.$

  (v):

  if $\langle (o_1,o_2):\mathbf{r} , \bowtie , k\rangle \in C_{\mathcal {F}},$ then $\langle (\beta (o_1),\beta (o_2)), \bowtie , k\rangle \in \mathbf{r} ^{\mathcal {S}}.$

Second, we use these two mappings to direct the expansion rules’ applications as shown in Table 2. As shown in Table 2, the expansion rules $\lnot \ge$, $\lnot \le$, $\cap \ge$, $\cap \le$, $\cup \ge$, $\cup \le$, $\exists \ge$, $\exists \le$, $\forall \ge$, $\forall \le$ are the common parts to fuzzy $\mathcal {ALC}$ and Straccia defines two mappings to guide the application of these expansion rules. Thus, we do not elaborate the proof of the common expansion rules. For the proof of these rules, we refer the reader to Straccia (2001). We only elaborate the rest rules as follows:

The expansion rule “$\exists \mathbf{r} \ge$” is utilized to the fuzzy concept of the form $\langle \exists (T_1,T_2).\mathbf{r} , \ge , k\rangle \in L(x)$. By the condition (ii), this implies $\langle \alpha (x), \ge , k\rangle \in (\exists (T_1,T_2).\mathbf{r} )^{\mathcal {I}}$. Hence, there are two elements $e_1,e_2 \in \Delta _{\mathcal {S}}$ such that $\langle (\alpha (x),\beta (e_1)), \ge , k\rangle \in (T_1)^{\mathcal {I}}$, $\langle (\alpha (x),\beta (e_2)), \ge , k\rangle \in (T_2)^{\mathcal {I}}$ and $\langle (e_1,e_2)$:$\mathbf{r} , \le , k\rangle \in (C)^{\mathcal {I}}$. Because there is no a $\langle T_1,T_2\rangle$-successor $\langle o_1,o_2\rangle$ of x in $\mathcal {F}$ s.t. $L(\langle x, o_1\rangle ) = \{\langle T_1, \ge , k\rangle \}$, $L(\langle x, o_2\rangle ) = \{\langle T_2, \ge , k\rangle \}$ and $\langle \mathbf{r} (o_1, o_2), \ge , k\rangle \in C_{\mathcal {F}}(x)$, the rule can add a $\langle T_1,T_2\rangle$-successor $\langle o_1,o_2\rangle$ of x, a set $L(\langle x, o_1\rangle ) = \{\langle T_1, \ge , k\rangle \}$, $L(\langle x, o_2\rangle ) = \{\langle T_2, \ge , k\rangle \}$, and add $\langle \mathbf{r} (o_1, o_2), \ge , k\rangle$ to $C_{\mathcal {F}}(x)$. Thus, we can obtain that there is a $\langle T_1,T_2\rangle$-successor $\langle o_1,o_2\rangle$ of x s.t. $\beta (o_1) = e_1$ and $\beta (o_2) = e_2$. As a result, the rule is utilized s.t. $\alpha$ and $\beta$ satisfy (ii), (iii), (iv) and (v) w.r.t $\mathcal {F}$. Similarly, for the $\exists \mathbf{r} \le$ rule, $\alpha$ and $\beta$ satisfy (ii), (iii), (iv) and (v) w.r.t $\mathcal {F}$.

Obviously, the two mappings $\alpha$ and $\beta$ satisfy all five conditions. Hence, by the applications of expansion rules, we can obtain a complete $\mathcal {F}$

Finally, we prove that the obtained completion forest $\mathcal {F}$ is clash-free.

Since the (i) and (ii) imply that there are no two conjugated triples, $\mathcal {F}$ does not contain a clash. Again Since the input f-${\mathcal {ALC}}({\mathcal S})$ ABox $\mathcal {A}$ is consistent and fuzzy spatial concrete domain $\mathcal {S}$ is admissible, the concrete domain constraint $C_{\mathcal {F}}$ is concrete domain satisfiable.

Therefore, by the applications of the expansion rules, we obtain a completion forest which is a complete and clash-free. This together with Theorem 2 ensures that the tableau algorithm is completeness. $\square$

As discussed in Theorem 1, fuzzy spatial concrete domain $\mathcal {S}$ is admissible and $\mathcal {S}$ -satisfiability is in NP-complete. Together with Theorems 2, 3, and 4, we get the following theorem about the decidability:

Theorem 5

(Decidability) The consistency problem of fuzzy description logic f-${\mathcal {ALC}}({\mathcal S})$ ABox w.r.t TBox $\mathcal {T}= \emptyset$ is decidable.

According to Theorem 5, it is shown that the decision procedure proposed in Sect. 6.1 is correct, i.e., the proposed decision procedure can correctly determine the f-${\mathcal {ALC}}({\mathcal S})$ ABox $\mathcal {A}$ consistency problem w.r.t an empty TBox $\mathcal {T}$.

Now, we discuss and analyze simply the complexity of the above reasoning problem with f-${\mathcal {ALC}}({\mathcal S})$. For crisp $\mathcal {ALC}$ (Schmidt-Schau and Smolka 1991), Lutz (1999) shows that the $\mathcal {ALC}$-concepts satisfiability problem w.r.t an empty TBox is PSPACE-complete. Tobies (2001) points out that the $\mathcal {ALC}$ ABox consistency problem w.r.t an empty TBox is also PSPACE-complete. For $\mathcal {ALC}$ DL with concrete domains $\mathcal {D}$, Lutz summaries that if $\mathcal {D}$ is admissible and $\mathcal {D}$-satisfiability problem can be decided in NP-complete, the complexity of the pure ${\mathcal {ALC}}({\mathcal D})$-concept satisfiability then is PSPACE-complete (Lutz 2002a, b). For the case of fuzzy $\mathcal {ALC}$, Straccia (2001) shows that fuzzy extensions of description logics have no impact from a computational complexity point of view. In other words, the inference problem of fuzzy DLs is in the same complexity classes as the corresponding crisp DLs. Since our proposed tableau algorithm is based on fuzzy $\mathcal {ALC}$ and $\mathcal {ALC}$ with concrete domains $\mathcal {D}$ and the idea of our decision procedure is similar to the one of the two DLs, the complexity of f-${\mathcal {ALC}}({\mathcal S})$ consistency is at the same level as the crisp ${\mathcal {ALC}}({\mathcal S})$ consistency. Again since fuzzy spatial concrete domain $\mathcal {S}$ is admissible and $\mathcal {S}$-satisfiability is in NP-complete, we can obtain the following complexity result:

Theorem 6

f-${\mathcal {ALC}}({\mathcal S})$-ABox consistency problem w.r.t an empty TBox is PSPACE-complete.

7 Conclusion and future work

In this work, we address a fuzzy spatial extension of description logic called f-${\mathcal {ALC}}({\mathcal S})$. In order to represent fuzzy spatial objects and handle their fuzzy topological relationship, we first establish a fuzzy spatial concrete domain $\mathcal {S}$ which includes fuzzy regions and their fuzzy spatial relationships. Then, we introduce the admissible $\mathcal {S}$ to the well-known fuzzy $\mathcal {ALC}$ DL and present a fuzzy spatial extension of DL called f-${\mathcal {ALC}}({\mathcal S})$. At the same time, the formal definitions of the syntax structure, semantic interpretation and knowledge base are given. Moreover, by taking an example of an f-${\mathcal {ALC}}({\mathcal S})$ knowledge base, we illustrate that how the language f-${\mathcal {ALC}}({\mathcal S})$ can be used to model fuzzy spatial relations. Then, we propose a decision procedure for f-${\mathcal {ALC}}({\mathcal S})$ to determine the consistency problem of fuzzy description logic f-${\mathcal {ALC}}({\mathcal S})$ ABox $\mathcal {A}$ with an empty TBox. Finally, we show that the decision procedure is correct and the consistency problem is decidable and PSPACE-complete. f-${\mathcal {ALC}}({\mathcal S})$ allows us to represent and reason fuzzy spatial knowledge on the Semantic Web and has better expressive and reasoning ability for fuzzy spatial knowledge.

As far as future work, we aim at investigating the complexity of the proposed reasoning algorithm in detail. Moreover, we will determine the consistency problem of w.r.t. acyclic TBoxs $\mathcal {T}$ or general TBox $\mathcal {T}$. Since our technology is still in the stage of theoretical research, we will develop a reasoner in the future work. Also fuzzy spatial description logics are the foundation theory of fuzzy spatial Semantic Web and fuzzy spatial ontologies. Thus, we will construct fuzzy spatial OWL ontologies based on our current work.