1 Introduction

Fuzzy description logics have been studied for over two decades, with the aim of providing logic-based knowledge representation and reasoning algorithms capable of dealing with imprecise knowledge. They have been employed to this end in various applications, ranging from image analysis [35] and ambient intelligence [37] to software design [36]. These applications are supported by numerous tools for constructing and reasoning with FDL ontologies [11, 12, 14, 50, 58, 61].

In FDLs, the classical binary truth values true and false are extended to more than two or even infinitely many truth values. Starting with [52, 60], a whole variety of tableau-based reasoning algorithms were developed for such logics. In addition to these extensions of classical DL algorithms, new methods based on crispification, i.e., a reduction to reasoning in classical DLs, were proposed, which are, however, restricted to finitely valued FDLs.

It came as a big surprise when it was pointed out in [9] that several of the existing tableau-based algorithms for infinitely valued FDLs were not sound. The main culprit turned out to be the presence of terminological cycles induced by general concept inclusions (GCIs), and the resulting loss of the finite model property. Reasoning in several FDLs was later found to be undecidable when allowing GCIs [6, 7, 33, 34]. This raised serious questions about the decidability of FDLs in general, which until then had been taken for granted.

The goal of this project was a detailed complexity analysis of the landscape of fuzzy description logics in order to delimit the undecidable logics from the decidable ones. This task was complicated by the large number of FDLs available. Starting from the known decidable and undecidable special cases, we aimed to derive general conditions for proving (un)decidability of large classes of FDLs, in particular in the presence of GCIs. In case of decidability, we also wanted to determine the precise computational complexity.

2 Fuzzy Description Logics

Description logics (DLs) [4] are a family of logics whose members are determined by the constructors and axioms they use to model the knowledge of an application domain. Concept constructors are employed to build concepts, which are expressions describing sets of domain elements with common properties. Roles describe binary relations between objects and are used within concept constructors. Assertional axioms state properties of named individuals, while terminological axioms formulate general knowledge that holds for all domain elements. Reasoning can be used to obtain additional knowledge about the domain under consideration. In this paper, we consider consistency as the main reasoning task; this task corresponds to deciding whether a given ontology (i.e., a collection of axioms) has a model.

The syntax of an FDL is based on that of a classical DL; however, beyond the choice of constructors and axioms, the definition of an FDL has additional degrees of freedom. While all FDLs use more than two truth values, one can choose whether these are represented by all rational numbers in the interval [0, 1] (infinitely valued semantics), or a finite set of truth degrees arranged in a lattice (finitely valued semantics). In the former case, FDLs can use either the Zadeh semantics [62] to interpret the constructors, or a semantics based on a (continuous) triangular norm (t-norm) [38, 39], of which uncountably many exist. Since the latter semantics do not preserve all classical equivalences between constructors, it makes sense to consider additional constructors, e.g., an implication constructor in addition to the standard conjunction and negation; moreover, different negation functions have been proposed in the literature on FDLs.

FDLs also allow more degrees of freedom w.r.t. the form of axioms. Often, fuzzy axioms allow to formulate lower bounds on the truth degree of a given classical axiom, but some of our results also apply to crisp ontologies, where only the lower bound 1 is used. Additionally, axioms are sometimes allowed to fix the exact truth degree of an assertion, or compare the truth degrees of two assertions. The final choice concerns the class of interpretations considered for reasoning. Beside standard (or general) models, which are defined in a straightforward way by “fuzzifying” the classical semantics, witnessed models were proposed in [39], which yield a more intuitive semantics for some constructors.

3 Results

We have shown undecidability for large classes of FDLs. Many of these FDLs are undecidable even if the ontology is crisp; hence, undecidability emerges solely from the fuzzy semantics and not from the ability to state truth degrees other than true and false. As in the first undecidability results [6, 7] for FDLs, our proofs are based on reductions of the Post Correspondence Problem (PCP). To complement these results, we developed tableau- and automata-based reasoning methods for less expressive FDLs, e.g. based on finitely valued or the infinitely valued (but still relatively simple) Gödel t-norm semantics. In the latter case, we had to develop new techniques since surprisingly many Gödel FDLs turned out to lack the finite model property.

Overall, our decidability and undecidability results cover most of the FDLs with t-norm-based semantics, as long as the underlying DL contains at least \(\mathcal {E\!L}\) and some kind of negation constructor. Not surprisingly, all FDLs with finitely valued semantics that we have investigated are decidable. For most of the decidable FDLs, we obtained tight complexity bounds.

For the DLs \(\mathcal {E\!L}\) and \(\mathcal {F\!L}_0\), which do not have negation, we obtained several results, although the overall picture remains incomplete. Reasoning in \(\mathcal {E\!L}\) is ExpTime-hard for many choices of t-norms, as opposed to the P-completeness observed in the classical case. A matching ExpTime upper bound was shown only for finitely valued semantics. The complexity of reasoning in fuzzy \(\mathcal {F\!L}_0\) under Gödel semantics does not increase in comparison to the classical case.

3.1 Undecidability Results: More Details

From the first undecidability proofs [6, 7, 33], we extracted criteria for an FDL to be able to express solvablity of a PCP instance. Basically, the logic must be able to express the search tree for a solution. This tree consists of nodes labeled with pairs (u, v) of words representing a candidate solution of the PCP. A solution is found when one node with label (w, w) is found.

In FDLs we encode words as numbers in the interval [0, 1] to simulate this search tree. The precise encoding depends on the fuzzy semantics considered. The framework proposed in [25] and extended in [15, 19] identifies five properties specifying structures that can be expressed by the constructors and axioms of a given FDL. Intuitively, these properties are: (i) all models can be forced to contain an element that encodes the root of the search tree; (ii) two words can be concatenated to construct the next candidate solution; (iii) new elements can be created to represent the child nodes of a given node; (iv) values can be transferred from nodes in the tree to their child nodes; and (v) the equality of two encodings of words can be expressed. These properties together imply undecidability of consistency in an FDL. We then identified several large classes of FDLs that satisfy each of these properties. For example, property (iii) always holds when dealing with witnessed models. Similarly, property (iv) is satisfied in \(\mathcal {E\!L}\) augmented with value restrictions.

Overall we obtain the undecidability results shown in Table 1 for FDLs over witnessed models. All the results hold for crisp terminologies. The first row considers completely crisp ontologies, i.e., where the assertional part is also crisp; in the second row, lower bounds on the degrees of assertions can be specified; and in the third row, exact values for such degrees can be stated. On the horizontal axis, we consider different combinations of constructors: the extension \(\mathfrak {N}\mathcal {E\!L}\) of \(\mathcal {E\!L}\) with the residual negation, the extension \(\mathfrak {N}\mathcal {AL}\) of \(\mathfrak {N}\mathcal {E\!L}\) with value restrictions, the extension \(\mathfrak {I}\mathcal {E\!L}\) of \(\mathfrak {N}\mathcal {E\!L}\) with implication, the very expressive extension \(\mathcal {SROIQ}\) of \(\mathfrak {I}\mathcal {E\!L}\) that underlies the standard ontology language OWL 2, the extension \(\mathcal {E\!LC}\) of \(\mathcal {E\!L}\) with involutive negation, and the extension \(\mathfrak {I}\mathcal {ALC}\) of \(\mathcal {E\!LC}\) with value restrictions and implication. An entry \(\mathsf {\Pi }\) denotes that the resulting FDL becomes undecidable when we consider the Product t-norm for the semantics, \(\textsf {\L } ^{(0,b)}\) denotes undecidability for a large class of t-norms that includes the Łukasiewicz t-norm (\(\textsf {\L } \)), and \(\otimes \) indicates undecidability for all (continuous) t-norms except the Gödel t-norm.

Table 1 Undecidability of consistency in FDLs
Full size table

Most results follow from the basic undecidable cases we identified [19]:

  • \(\mathfrak {N}\mathcal {E\!L}\) with crisp ontologies and \(\textsf {\L } ^{[0,b]}\)-t-norms,

  • \(\mathfrak {I}\mathcal {E\!L}\) with equality assertions and any t-norm except the Gödel t-norm,

  • \(\mathcal {E\!LC}\) with \(\ge \)-assertions and any t-norm except the Gödel t-norm, and

  • \(\mathcal {E\!LC}\) with crisp ontologies and the Product t-norm.

In [2], it was further shown that \(\mathfrak {N}\mathcal {AL}\) with equality assertions and the Product t-norm is undecidable. These results subsume all previously known undecidable cases [6, 7, 33], and prove undecidability of all logics for which correct tableau algorithms had been claimed to exist, but shown to be incorrect due to the lack of the finite model property. In [2], we discuss in depth the issues caused by infinitely valued semantics for existing tableau methods for FDLs, and highlight how the undecidability results exploit these weaknesses.

As described in the next section, most of these results are in fact tight, i.e., decidability holds for all other t-norms (shown in Table 1 by a gray background). In particular, all FDLs using the Gödel t-norm are decidable, even when they use both residual and involutive negation [22]. This covers most expressive DLs in use today, and leaves open only the special cases at the lower left and the upper right corners of Table 1. Regarding the former, it seems possible to extend the undecidability result of [2] to a larger class of t-norms, but a full classification remains open. In the latter case, it is arguable whether fuzzy semantics using the involutive negation, but none of the three basic t-norms Gödel, Łukasiewicz, or Product, make sense, and whether these open cases should be pursued further.

3.2 Decidability Results: More Details

We identified two main classes of decidable FDLs. The first concerns FDLs that use t-norms outside of the class \(\textsf {\L } ^{[0,b]}\), restricted to \(\ge \)-assertions, and without involutive negation. We have shown in [17] that the semantics of such logics degenerates to the underlying classical semantics. That is, if we remove all fuzzy degrees from a fuzzy ontology, the result is consistent in the classical sense iff the original ontology is consistent under the fuzzy semantics. This trivially yields the same complexity bounds as for the underlying classical DLs. These results hold even for very expressive DLs like \(\mathcal {SROIQ}\) (under the mentioned restrictions) [19]. It should be noted, however, that this reduction works only for deciding consistency; for other reasoning problems, decidability is still an open problem.

The second class of decidable FDLs are ones with the Gödel t-norm. Before our work, it was generally assumed that Gödel FDLs have the finite model property, and in particular the finitely valued model property, where reasoning can be restricted without loss of generality to models using only finitely many degrees of truth. The reason for this assumption was the strong similarity to the Zadeh semantics, which has these properties [53]. We have shown in [18] that this assumption is wrong; under Gödel semantics, the finitely valued model property fails already for extensions of \(\mathcal {E\!L}\) with either value restrictions or the implication constructor.

While the lack of the finite model property in other FDLs led to undecidability, we were able to show that the Gödel t-norm preserves decidability. We observed that the precise truth degrees used in models do not matter, but only the order relations among them. Thus, it suffices to consider abstract models, which specify only a total order on the values relevant for the consistency of the ontology. Based on this abstraction, we developed an automata-based reasoning approach [18], which is closely related to the approach for finitely valued FDLs described in Sect. 3.3 below.

We have also combined the automata approach with the crispification method typically used for finitely valued FDLs [30]. While applicable to relatively expressive DLs, this approach depends on the tree model property, which does not hold in \(\mathcal {SROIQ}\) [59], but in its sublogics \(\mathcal {SRIQ}\), \(\mathcal {SROQ}\), and \(\mathcal {SROI}\) [32]. The combined approach allowed us to show that, in most cases, the complexity of reasoning remains the same as the one for the underlying classical DLs.

By lifting the tableau algorithm of [41, 42] to our order abstraction, we extended our decidability results to \(\mathcal {SROIQ}\) with Gödel semantics [22]. In contrast to previous tableau algorithms dealing with GCIs, ours uses a correct blocking condition that is based on a finite representation of possibly infinite models. Our algorithm is related to the technique for Zadeh semantics presented in [51], but considers infinitely many values, and supports non-crisp concept and role inclusions. To deal with the latter, we developed a fuzzy generalization of the automata-based technique from [42].

3.3 Finitely Valued FDLs

We investigated the complexity of FDLs with finitely valued semantics. Although lattice-based semantics had been proposed before [54], most research in this direction focused on finite total orders. The crispification approach, which was developed for such FDLs, did not provide precise complexity bounds due to a blow-up in the size of the resulting classical ontology [10, 13].

Our own work on this topic started with an automata-based construction that allowed us to show tight complexity bounds for a variety of finitely valued FDLs [23, 26, 29, 31]. We have shown consistency to be in ExpTime for DLs up to \(\mathcal {SHOI}\) (ExpTime-hardness already holds in the classical case [49]). When the terminology is restricted to being acyclic and all transitive roles are crisp, the classical complexity of PSpace in these DLs does not increase under finitely valued semantics. These results use the PSpace on-the-fly constructions from [5]. Using tableau methods and pre-completion [40], we were able to transfer these complexity results also to other reasoning problems [24, 28].

These approaches do not work for reasoning tasks like answering (fuzzy) conjunctive queries (CQs) over fuzzy ontologies. Answering CQs w.r.t. ontologies is an important extension of the classical problem of CQ answering in databases, which has recently received considerable attention [8, 47]. For FDLs, several fuzzy extensions of CQs have been proposed [48, 56, 57]. In [21, 43], we have extended the crispification approach to answer fuzzy CQs in finitely valued FDLs. Notably, [21] presents a pre-processing step that avoids the exponential blow-up of previous methods, yielding tight complexity bounds in many cases. We also showed that some previous crispification approaches are incorrect for number restrictions. An evaluation of a prototype implementation of our approach on top of DeLorean [11] demonstrates that the pre-processing effectively reduces the size of the resulting ontologies, and thus answering fuzzy CQs becomes feasible under finitely valued semantics.

A different approach for fuzzy CQ answering for the inexpressive FDL DL-Lite was developed independently in [45]. There, the rewriting approach from classical DL-Lite is extended to its Gödel variant, and conditions under which this technique yields correct result also for other t-norms are investigated.

3.4 Fuzzy Extensions of Inexpressive DLs

The final area we considered were fuzzy extensions of inexpressive DLs, like \(\mathcal {E\!L}\) and \(\mathcal {F\!L}_0\). In these logics, consistency is trivial, and hence research focuses on deciding subsumption between concepts.

For the Gödel t-norm, it was known that the complexity of subsumption in \(\mathcal {E\!L}\) remains P-complete [3, 44]. In contrast, we showed a co-NP lower bound for a large class of t-norms including the Łukasiewicz t-norm [27], using a reduction from the (complement of the) vertex cover problem. In [16] we further raised this lower bound to ExpTime, even for finitely valued extensions of \(\mathcal {E\!L}\). For fuzzy \(\mathcal {E\!L}\) based on finitely valued variants of the Łukasiewicz t-norm, this means that subsumption reasoning is ExpTime-complete [26], and together with [44] we obtain a complete characterization of the complexity of fuzzy extensions of \(\mathcal {E\!L}\) with finite t-norms. However, the precise complexity remains open for the infinitely valued Łukasiewicz and Product t-norms.

In \(\mathcal {F\!L}_0\), subsumption is ExpTime-complete already in the classical case [3]. Hence, by the results of Sect. 3.2, the fuzzy variant of \(\mathcal {F\!L}_0\) with the Gödel t-norm has the same complexity. We showed that, when restricting to cyclic terminologies, the complexity of the Gödel extension of \(\mathcal {F\!L}_0\) reduces to PSpace, while for acyclic terminologies it belongs to co-NP  [20]. To show these results, we employed a weighted generalization of the automata construction used in the classical case [1].

4 Outlook

While this project has substantially increased the state of research regarding decidability and complexity of FDLs, there remain a number of open issues.

For instance, the picture of decidability and complexity for the case of general models is not as clear as the one described for witnessed models in Table 1, although some results have been obtained [15]. Extensions of FDLs with concrete domains [46, 55] and other non-logical constructors need also to be studied in more detail. Nevertheless, our results provide an important map of the complexity landscape of fuzzy description logics, which can aid researchers and modeling experts alike in choosing a fuzzy description logic suitable for their needs.

Since some of the reasoning algorithms are extensions of the classical ones used in current DL reasoners, it is conceivable that these reasoners can be adapted to deal with FDLs, at least under finitely valued or Gödel semantics. Tableau algorithms that can deal with GCIs under Zadeh semantics have already been implemented [14, 50]. Providing tableau reasoners for different fuzzy semantics will help to speed up the adoption of FDLs for modeling purposes in applications.