Role-Value Maps and General Concept Inclusions in the Minimal Description Logic with Value Restrictions or Revisiting Old Skeletons in the DL Cupboard

Description logics (DLs) [6] are a well-investigated family of logic-based knowledge representation formalisms, which are used to define ontologies in applications domains such as the semantic web [9, 19] and in biology and medicine [20]. DLs are descended from semantic networks [28, 29] and frames [26] via the knowledge representation system KL-ONE [17]. The design goal of KL-ONE was, on the one hand, to provide its users with a knowledge representation (KR) language that is equipped with a well-defined syntax and a formal, unambiguous semantics, which was not always true for early KR approaches such as semantic networks and frames. On the other hand, reasoning over knowledge bases written in this language was supposed to be tractable (i.e., realizable by polynomial-time inference procedures) [15]. Thus, it came as a considerable shock to the community when it was shown that the second requirement is not satisfied by the language employed by KL-ONE for two independent reasons.

On the one hand, KL-ONE provided its users with the concept constructor role-value maps (RVMs), which can be employed to link role successor sets. For example, the concept described by the RVMcollects all individuals that know all the friends of their children. The general form of such an RVM is \((r_1\circ \cdots \circ r_m\subseteq s_1\circ \cdots \circ s_n)\), where \(r_1,\ldots ,s_n\) are roles (i.e., binary predicates). It was shown in [30] that the presence of RVMs actually makes reasoning in KL-ONE undecidable. As a consequence, general RVMs were removed from KL-ONE-based KR languages, and are not available in any of the DLs employed by today’s DL systems. One possibility for avoiding the undecidability caused by RVMs is to restrict the roles occurring in them to being functional. This approach was employed by the CLASSIC system [14], where the corresponding constructor is called the same-as constructor. However, using same-as in place of RVMs only overcomes the undecidability problem if no general concept inclusions (GCIs) are available in the terminological formalism [5].

An alternative approach for restricting RVMs with the goal of achieving decidability is to consider global role-value maps in which role composition on the right-hand side is disallowed. In contrast to the local RVMs used in the KL-ONE system, a global RVM is not a concept constructor, but a terminological axiom, which states that the inclusion must hold for all individuals in the interpretation domain. For example, while \((\mathsf {child}\circ \mathsf {friend}\subseteq \mathsf {knows})\) is a concept that is interpreted as the set of individuals that know all the friends of their children, the global RVMstates that all individuals in the interpretation domain know all the friends of their children.¹ Global RVMs may still cause undecidability [3, 8] unless one imposes additional restrictions. For the inexpressive DL \(\mathcal{EL}\) [4, 10], adding global RVMs of the form \((r_1\circ \cdots \circ r_m\sqsubseteq s)\) leaves reasoning not only decidable, but also tractable even in the presence of GCIs [3, 4]. For more expressive DLs, additional restrictions on such RVMs need to be imposed to keep reasoning decidable [22, 24].

On the other hand, KL-ONE provided its users with the concept constructors conjunction (\(\sqcap\)) and value restriction (\(\forall r. C\)). For example, using these constructors one can build the conceptwhich describes the persons all of whose children have only nice friends. It was shown in [27] that the subsumption problem in the DL \(\mathcal{FL}_0\), which has only these two constructors, is coNP-hard in the presence of the simplest terminological formalism, which are so-called acyclic TBoxes. For cyclic TBoxes, the complexity increases to PSpace [1, 25], and for general TBoxes consisting of GCIs even to ExpTime [4, 21]. Thus, w.r.t. general TBoxes, subsumption reasoning in \(\mathcal{FL}_0\) is as hard as in \(\mathcal{ALC}\), its closure under negation.

In the present paper, we first reconsider this ExpTime-hardness result. The proof in [4] leads to a rather long chain of reductions, which makes it hard to understand the reasons for ExpTime-hardness and to reuse the proof ideas for other DLs. The proof of ExpTime-hardness given in [21] is by a reduction from deciding the winner in pushdown games [31], but the argument used for showing the correctness of this reduction is based on a non-trivial proof-theoretic characterization of subsumption in \(\mathcal{FL}_0\) w.r.t. general TBoxes. In Sect. 3, we provide a new reduction from the problem of deciding the winner in countdown games [23], for which we must show, among other things, that we can express (binary representations) of natural numbers and subtraction of such numbers in \(\mathcal{FL}_0\). ExpTime-hardness for pushdown games and for countdown games was respectively shown in [23, 31] by direct reductions from the problem of the acceptance of a word by a linearly space-bounded alternating Turing machine.

In the second part of the paper (Sects. 4, 5), we investigate the effect that adding RVMs has on the decidability of subsumption in \(\mathcal{FL}_0\). On the one hand, we introduce two classes of global RVMs that leave subsumption without GCIs decidable. A simple example of a class of RVMs that satisfy both restrictions are length-preserving RVMs. On the other hand, we show that the restrictions made to achieve decidability are really needed: (1) in the presence of GCIs, even adding a single length-preserving RVM can cause undecidability; (2) for unrestricted RVMs, we give a simpler proof of the result first shown in [30] that undecidability even holds without GCIs. The results (1) and (2) are independent of whether global or local RVMs are used.

Some of the more technical proofs of these results are not given in detail here. They can be found in [12].

In Description Logic, concept constructors are used to build complex concepts out of concept names (unary predicates) and role names (binary predicates). A particular DL is determined by the available constructors. Starting with mutually disjoint countably infinite sets \(N_C\) and \(N_R\) of concept and role names, respectively, the set of \(\mathcal{FL}_0\) concepts is inductively defined as follows:The semantics of \(\mathcal{FL}_0\) concepts is defined using first-order interpretations \({\mathcal{I}} = (\Delta {^{\mathcal{I}}}, \cdot {^{\mathcal{I}}})\) consisting of a non-empty domain \(\Delta {^{\mathcal{I}}}\) and an interpretation function \(\cdot {^{\mathcal{I}}}\) that assigns a set \(A{^{\mathcal{I}}} \subseteq \Delta {^{\mathcal{I}}}\) to each concept name A, and a binary relation \(r{^{\mathcal{I}}} \subseteq \Delta {^{\mathcal{I}}} \times \Delta {^{\mathcal{I}}}\) to each role name r. This function is extended to \(\mathcal{FL}_0\) concepts as follows:A (general) \(\mathcal{FL}_0\)TBox \({\mathcal{T}}\) is a finite set of general concept inclusions (GCIs), which are expressions of the form \(C \sqsubseteq D\) for \(\mathcal{FL}_0\) concepts C, D. The interpretation \(\mathcal{I}\) is a model of \({\mathcal{T}}\) if it satisfies all the GCIs in \({\mathcal{T}}\), i.e. \(C{^{\mathcal{I}}} \subseteq D{^{\mathcal{I}}}\) holds for all GCIs \(C \sqsubseteq D\) in \({\mathcal{T}}\). Given an \(\mathcal{FL}_0\) TBox \({\mathcal{T}}\) and two \(\mathcal{FL}_0\) concepts C, D, we say that C is subsumed by D (denoted as \(C \sqsubseteq _{{\mathcal{T}}} D\)) if \(C{^{\mathcal{I}}} \subseteq D{^{\mathcal{I}}}\) for all models \(\mathcal{I}\) of \({\mathcal{T}}\). These two concepts are equivalent (denoted as \(C \equiv _{\mathcal{T}} D\)) if \(C \sqsubseteq _{\mathcal{T}} D\) and \(D \sqsubseteq _{\mathcal{T}} C\). If the TBox is empty, we write \(C \sqsubseteq D\) and \(C \equiv D\) instead of \(C \sqsubseteq _\emptyset D\) and \(C \equiv _\emptyset D\).

For \(\mathcal{FL}_0\), the subsumption problem w.r.t. general TBoxes is ExpTime-complete: the upper bound follows from the well-known ExpTime upper bound for \(\mathcal{ALC}\) [8], which contains \(\mathcal{FL}_0\) as a sublogic. Previous proofs of the lower bound can be found in [4, 21]. In the next section, we will provide a new proof of this hardness result.

Without TBox, subsumption and equivalence in \(\mathcal{FL}_0\) can be characterized using inclusion of formal languages. This characterization relies on transforming \(\mathcal{FL}_0\) concepts into an appropriate normal form as follows. First, the semantics given to the concept constructors in \(\mathcal{FL}_0\) implies that value restrictions distribute over conjunction, i.e., for all \(\mathcal{FL}_0\) concepts C, D and roles r it holds that \(\forall r. (C \sqcap D) \equiv \forall r. C \sqcap \forall r. D\). Using this equivalence as a rewrite rule from left to right, every \(\mathcal{FL}_0\) concept can be transformed into an equivalent one that is either \(\top\) or a conjunction of concepts of the form \(\forall r_1\cdots \forall r_n. A\), where \(r_1, \ldots , r_n\) are role names and A is a concept name. Such a concept can be abbreviated as \(\forall w. A\), where \(w= r_1 \ldots r_n\) is a word over the alphabet \(N_R\). Note that \(n = 0\) means that w is the empty word \(\varepsilon\), and thus \(\forall \varepsilon .A\) corresponds to A. Furthermore, a conjunction of the form \(\forall w_1. A \sqcap \cdots \sqcap \forall w_m. A\) can be written as \(\forall L.A\) where \(L \subseteq N_R^*\) is the finite language \(\{w_1, \ldots , w_m\}\). We use the convention that \(\forall \emptyset .A\) corresponds to the top concept \(\top\). Thus, any two \(\mathcal{FL}_0\) concepts C, D containing only the concept names \(A_1,\ldots ,A_\ell\) can be represented aswhere \(K_1, L_1, \ldots , K_\ell , L_\ell\) are finite languages over the alphabet of role names \(N_R\). We call this representation the language normal form (LNF) of C, D.

If C, D have the LNFs shown above, then \(C\sqsubseteq D\) holds iff \(L_1\subseteq K_1, \ldots , L_\ell \subseteq K_\ell\) [11]. A similar characterization of subsumption can actually also be given in the presence of a TBox, but then \(K_1,\ldots ,L_\ell\) are regular languages represented by automata of size exponential in the size of \({\mathcal{T}}\) [7].

We give a new proof of the fact that subsumption in \(\mathcal{FL}_0\) w.r.t. a general TBox is ExpTime-hard. This proof is by reduction from the problem of deciding the winner in countdown games, which are two-player games for which deciding which player has a winning strategy is known to be ExpTime-complete [23].

As defined in [23], a countdown game is given by a weighted graph (S, T), where S is the finite set of states and \(T \subseteq S \times (\mathbb {N} \setminus \{0\}) \times S\) is the finite transition relation. If \(t = (s, d, s') \in T\), then we say that the duration of the transition t is d. A configuration of a countdown game is a pair (s, c), where \(s \in S\) is a state and \(c \in \mathbb {N}\). A move of a countdown game from a configuration (s, c) is performed in the following way: first Player 1 chooses a number d such that \(0 < d \le c\) and there is \(s'\in S\) with \((s,d,s') \in T\); then Player 2 chooses a transition \((s, d, s')\in T\) of duration d; the new configuration resulting from this move is then \((s', c-d)\). There are two types of terminal configurations, i.e., configurations (s, c) in which no more moves are available. If \(c = 0\) then the configuration (s, c) is terminal and is a winning configuration for Player 1. If for all transitions \((s,d,s') \in T\) from the state s we have that \(d> c\), then the configuration (s, c) is terminal and it is a winning configuration for Player 2. The algorithmic problem of deciding the winner in countdown games is the following problem: given a weighted graph (S, T) and a configuration \((s_0,c_0)\), where all the durations of transitions and the number \(c_0\) are assumed to be represented in binary, to determine whether Player 1 has a winning strategy from the configuration \((s_0,c_0)\). Formally, a winning strategy can be described by a tree whose nodes are labeled with configurations. The root is labeled with the initial configuration, and the leaves are labeled with terminal configurations that are winning configurations for Player 1. A node labeled with a non-terminal configuration (s, c) has successor nodes that correspond to one choice of Player 1 followed by all possible choices of Player 2, i.e., to obtain the successors of this node, one chooses one number d that corresponds to an eligible choice of Player 1, and then adds successors nodes for all possible choices that Player 2 has: for each transition \((s,d,s')\in T\) a node with label \((s',c-d)\) is added. Theorem 2 in Section 4.2 of [23] shows that the problem of deciding whether such a winning strategy exists for a given countdown game and initial configuration is ExpTime-complete by a reduction from the word problem for linearly space-bounded alternating Turing machine.

When describing such games in a logic, one must, on the one hand, be able to express the alternation of choices between the players. In the presence of both existential and universal quantifiers, this is usually easy to achieve, but it is less clear how to do this in \(\mathcal{FL}_0\), which has only universal quantification at its disposal. We will discuss at the end of this section how this is achieved in our reduction. In [21], this point is somewhat hidden in the proof-theoretic argument. On the other hand, one must be able to describe the moves and the winning conditions, which for countdown games means that one must be able to represent subtraction and a zero test. Again, it is quite surprising that this is possible in a logic like \(\mathcal{FL}_0\), which has conjunction as its only Boolean operation. In [21], this part appears to be easier since configurations in pushdown games are words over a finite alphabet, which can directly be represented using sequences of value restrictions.

Given the ExpTime-hardness result for deciding the winner in countdown games shown in [23], this proposition yields the following hardness result for \(\mathcal{FL}_0\).

Before closing this section, let us analyze how our reduction has addressed the two main requirements for such a reduction mentioned above Proposition 1. First, consider the alternation of choices between the players. The fact that it is sufficient that one choice of Player 1 is successful is expressed by the GCI 2. In fact, if one considers the contraposition of this GCI, then it becomes clear that is says: if Player 1 does not fail, then it already has reached a winning configuration or there is a successor configuration in which it does not fail. The universal quantification over the moves of Player 2 is expressed using the GCI 1. Regarding the representation of numbers in binary, one should note that we cannot enforce that every individual is associated with only one number. In fact, since \(\mathcal{FL}_0\) cannot express disjointness of concepts, we cannot prevent an individual from belonging to both \(\mathsf {b}_{i}\,{=}\,{0}\) and \(\mathsf {b}_{i}\,{=}\,{1}\). This is not a problem for the following reasons. Of course, when constructing an interpretation from a winning strategy, one can just build a counter-interpretation to the subsumption where every element has a unique associated number, which is given by the strategy tree. Conversely, having more numbers in a counter-interpretation can only make satisfying the conditions for a winning strategy formulated by the GCIs harder to achieve. By removing superfluous elements and numbers, one can modify the given interpretation to one that looks like the one depicted in Fig. 1 and still satisfies all GCIs. From this, the winning strategy can then be extracted.

As already mentioned in the introduction, role-value maps come in two variants [8]: local RVMs as originally introduced in KL-ONE are concept constructors whereas global RVMs are axioms that constrain the interpretation of roles. To be more precise,In the presence of GCIs, local RVMs can express global ones since the global RVM \((r_1 \circ \cdots \circ r_m \sqsubseteq s_1 \circ \cdots \circ s_n)\) has the same models as the GCI \(\top \sqsubseteq (r_1 \circ \cdots \circ r_m \subseteq s_1 \circ \cdots \circ s_n)\).

To simplify notation, we write \(t_1\ldots t_k\) in place of \(t_1\circ \cdots \circ t_k\), and again view this expression as a word over the alphabet of role names. Thus, a set \({\mathcal{T}}\) of global RVMs can be written as \({\mathcal{T}} = \{u_1 \sqsubseteq v_1,\ldots ,u_k \sqsubseteq v_k\}\) where \(u_1,\ldots , v_k\in N_R^*\). Such a set induces the following string-rewriting relation [13] between words over \(N_R\):As usual, we denote the reflexive, transitive closure of \(\rightarrow _{\mathcal{T}}\) as \(\mathrel {\displaystyle \mathop {\rightarrow }^{*}}_{\mathcal{T}}\). Given a formal language L over \(N_R\), i.e., a subset of \(N_R^*\), we now define the languageswhich can be used to characterize subsumption w.r.t. \({\mathcal{T}}\) as follows.

Regarding the proof of this theorem, first note that 2. and 3. are easily seen to be equivalent. In fact, given a word \(w\in L_i\), we have \(w\in K_i^{\downarrow _{\mathcal{T}}}\) iff \(\exists y\in K_i\ \text{ with }\ y\mathrel {\displaystyle \mathop {\rightarrow }^{*}}_{\mathcal{T}} w\) iff \(\exists y\in K_i\ \text{ with }\ y\in \{w\}^{\uparrow _{\mathcal{T}}}\) iff \(\{w\}^{\uparrow _{\mathcal{T}}} \cap K_i\ne \emptyset\).

Our proof of \(2.\Rightarrow 1.\) uses the following proposition, which is an easy consequence of the semantics of global RVMs and value restrictions, and our definition of \(\rightarrow _{\mathcal{T}}\).

This proposition yields that \(C \sqsubseteq _{{\mathcal{T}}} \forall w. A_i\) holds for all \(w \in K_i^{\downarrow _{\mathcal{T}}}\) and all \(i, 1\le i\le \ell\). If \(L_i\subseteq K_i^{\downarrow _{\mathcal{T}}}\), then this implies that \(C \sqsubseteq _{\mathcal{T}} \forall L_i. A_i\) for all \(i, 1\le i\le \ell\), and thus we have \(C \sqsubseteq _{{\mathcal{T}}} D\).

We show \(1.\Rightarrow 2.\) by contraposition. Thus, assume that there is an i and a word \(w = t_1\ldots t_p\) such that \(w\in L_i{\setminus } K_i^{\downarrow _{\mathcal{T}}}\). We use w and i to build a counterexample to the subsumption \(C\sqsubseteq _{\mathcal{T}} D\), i.e., a model \(\mathcal{I} _{w,i}\) of \({\mathcal{T}}\) in which \(C{^{\mathcal{I}}} \not \subseteq D{^{\mathcal{I}}}\). To construct \(\mathcal{I} _{w,i}\), we start with a sequence of individuals \(d_0,\ldots ,d_p\) and connect them with the roles in w, i.e., we set \((d_0,d_1)\in t_1^{\mathcal{I} _{w,i}},\ldots ,(d_{p-1},d_p)\in t_p^{\mathcal{I} _{w,i}}\). Then we extend \(\mathcal{I} _{w,i}\) with additional individuals in order to add the role paths required by the RVMs in \({\mathcal{T}}\). Assume that \(r_1\ldots r_m \sqsubseteq s_1\ldots s_n\) is a RVM in \({\mathcal{T}}\), and there are two individuals d, e in the domain of \(\mathcal{I} _{w,i}\) such that \(e\in (r_1\circ \cdots \circ r_m)^{\mathcal{I} _{w,i}}(d)\), but \(e\not \in (s_1\circ \cdots \circ s_n)^{\mathcal{I} _{w,i}}(d)\). Then we add new individuals \(f_1,\ldots ,f_{n-1}\) to the domain of \(\mathcal{I} _{w,i}\) and connect them via the roles \(s_1,\ldots ,s_n\) as follows: \((d,f_1)\in s_1^{\mathcal{I} _{w,i}},(f_1,f_2)\in s_2^{\mathcal{I} _{w,i}},\ldots ,(f_{n-1},e)\in s_n^{\mathcal{I} _{w,i}}\). In general, this process needs to be iterated infinitely, and the resulting interpretation \(\mathcal{I} _{w,i}\) is the limit obtained by this infinite process. To ensure that this interpretation indeed satisfies all RVMs in \({\mathcal{T}}\), the extension process needs to be organized in a fair way, i.e., for every pair of individuals d, e and RVM \(r_1\ldots r_m \sqsubseteq s_1\ldots s_n\) violated by this pair (as described above), we must eventually apply an extension step that removes this violation. This is, however, not hard to achieve (e.g., by labeling such violations with the iteration step in which they were introduced, and then always choosing one of the oldest violations). Finally, we interpret concept names in \(\mathcal{I} _{w,i}\) as follows: all individuals except for \(d_p\) belong to all concept names, whereas \(d_p\) belongs to all concept names except for \(A_i\). The following proposition is now easy to show.

Since \(\mathcal{I} _{w,i}\) is a model of \({\mathcal{T}}\), it is sufficient to show that \(d_0\in C^{\mathcal{I} _{w,i}}\setminus D^{\mathcal{I} _{w,i}}\). First, suppose that \(d_0\in C^{\mathcal{I} _{w,i}}\) does not hold. By our definition of the interpretation of concept names in \(\mathcal{I} _{w,i}\), this can only be the case if there is a word \(u\in K_i\) such that \((d_0, d_p) \in u^{\mathcal{I} _{w,i}}\). The above proposition yields \(u \mathrel {\displaystyle \mathop {\rightarrow }^{*}}_{\mathcal{T}} w\), and thus \(w\in K_i^{\downarrow _{\mathcal{T}}}\), contradicting our choice of w. Consequently, we must have \(d_0\in C^{\mathcal{I} _{w,i}}\). Finally, we have \(d_0 \notin D^{\mathcal{I} _{w,i}}\) since \(w\in L_i\), \((d_0,d_p)\in w^{\mathcal{I} _{w,i}}\), and \(d_p\notin A_i^{\mathcal{I} _{w,i}}\). This completes the proof of Theorem 2.

In order to derive decidability results for subsumption w.r.t. RVMs in \(\mathcal{FL}_0\) from this theorem, we need to find restrictions under which the condition 2. or 3. is decidable. We say that the finite set of RVMs \({\mathcal{T}}\) is downward (upward) admissible if for every finite language L we can effectively compute a representation of \(L^{\downarrow _{\mathcal{T}}}\) (\(L^{\uparrow _{\mathcal{T}}}\)) for which the word problem is decidable. We say that \({\mathcal{T}}\) is admissible if it is downward admissible or upward admissible.

To the best of our knowledge, this is the first decidability result for RVMs where role composition is allowed on the right-hand side. On the one hand, one can use our result to find syntactic restrictions on global RVMs that ensure decidability.

For example, if all RVMs \(u_i\sqsubseteq v_i\) in \({\mathcal{T}}\) satisfy \(|u_i|\le |v_i|\), then \(L^{\downarrow _{\mathcal{T}}}\) is also finite (and thus trivially has a decidable word problem) and can effectively be computed. Thus, such a set of RVMs is downward admissible. Symmetrically \(|u_i|\ge |v_i|\) for all RVMs \(u_i\sqsubseteq v_i\) in \({\mathcal{T}}\) implies that \({\mathcal{T}}\) is upward admissible. On the other hand, one can also have downward (upward) admissible sets of RVMs where the languages \(L^{\downarrow _{\mathcal{T}}}\) (\(L^{\uparrow _{\mathcal{T}}}\)) are not necessarily finite, but one can compute a finite automaton or a pushdown automaton accepting them.

In general, one needs to analyze the specific set of RVMs \({\mathcal{T}}\) to find out whether a finite or pushdown automaton exists for the upward or downward languages. This is akin to the approach used in [22, 24] to deal with RVMs without composition of roles on the right-hand side, but for expressive DLs. There, the set of RVMs needs to satisfy a regularity restriction in order to obtain decidability.

First, we show that, even without GCIs, RVMs can cause undecidability in \(\mathcal{FL}_0\). This result was first proved in [30] for an extension of \(\mathcal{FL}_0\)⁵ with local role value maps of the form \((r_1 \circ \cdots \circ r_m = s_1 \circ \cdots \circ s_n)\), which in our notation can be written as \((r_1 \circ \cdots \circ r_m \subseteq s_1 \circ \cdots \circ s_n)\sqcap (s_1 \circ \cdots \circ s_n \subseteq r_1 \circ \cdots \circ r_m)\). Below, we will first show undecidability for global RVMS, and then extend this result to the case of local RVMs without TBox, using an approach first employed in [30]. We will say more about the connection between our proofs and the one in [30] after having presented our proofs.

Using a trick originally introduced in [30], we can easily transfer this undecidability result from global RVMs to local ones.

Regarding the comparison with the proof in [30], first note that global RVMs are not considered there, but one could easily adapt the approach in [30] to show undecidability also for global RVMs. Second, as mentioned above, the RVMs considered in [30] use equality rather than inclusion, which appears to be less expressive, and thus makes the undecidability result stronger. However, considering our reduction in the proof of Theorem 3, we see that we actually have the RVMs in both directions, and thus can replace them by ones using equality only. This is not the case for Corollary 2 since there the local RVMs \((r\subseteq s)\) and \((sr\subseteq s)\) are used only in one direction. In the general setting considered in that corollary, adding the RVMs in the other direction would not work. Basically, this is the reason why the proof in [30] uses a reduction from the word problem for finitely presented groups, rather than the word problem for finitely presented semigroups (which is the same as the word problem for string-rewriting systems employed in our proof). On a quite technical level, this is explained in [30] in a remark below the proof of Theorem 3.5. The main difference between the two proofs is, however, that we obtain our result as a simple consequence of the elegant characterization of subsumption in \(\mathcal{FL}_0\) with RVMs given in Theorem 2, whereas the proof of correctness of the reduction in [30] is rather technical.

Next, we show that, in the presence of GCIs, undecidability can also be caused by global RVMs that satisfy the admissibility condition introduced in the previous section. In fact, we will see that a single global RVM of the form \(tr\sqsubseteq rt\) is sufficient to obtain undecidability. Since this RVM is length-preserving, it is both downward and upward admissible.

Readers that are familiar with the undecidability proof for subsumption in \(\mathcal{ALC}\) with global RVMs given in [8], which is by reduction from the tiling problem, may think that the proof of the above theorem should be an easy adaptation of the proof in [8]. A closer look at that proof reveals, however, that it makes extensive use of concept constructors not available in \(\mathcal{FL}_0\) (such as negation, disjunction, and existential restrictions). In addition, it requires not only the RVM \(tr\sqsubseteq rt\), but also its backward direction \(rt\sqsubseteq tr\). The undecidability proof in [30] uses the concept constructors of \(\mathcal{FL}_0\) and local role-value maps. In addition to being local instead of global, the RVMs used there are not admissible since they contain the defining relations of a finitely presented group with undecidable word problem.

The main new contribution of the proof sketched below is thus to show that one can obtain the undecidability results for a single global RVM of the form \(tr\sqsubseteq rt\) also with the seriously restricted expressive power of \(\mathcal{FL}_0\).

We prove Theorem 4 by a reduction from the halting problem for deterministic Turing machines (DTMs). Without loss of generality, we consider DTMs that have a one-side infinite tape, where the left-most tape cell is marked using the special symbol $. Whenever the machine moves to the left onto this cell, in the next step it immediately goes to the right again and leaves the symbol $ and the state unchanged. We also assume that the machine can only go left or right (i.e., it cannot stay in place).

The machine starts with an “empty” tape, i.e., a tape where the left-most cell contains $ and all other cells contain the blank symbol B. The blank symbol and $ cannot be written by the machine. It halts when a special halting state halt is reached. For all other states, there is a transition for every possible tape symbol. Clearly, the question whether such a DTM halts when started with the initial state \(q_0\) on the empty tape is undecidable.

Let \(M = (Q, \varSigma , \delta , q_0)\) be such a DTM. In order to encode the halting problem for M into a subsumption problem, we assume without loss of generality that \(\{r, t\} \subseteq N_R\) (for “right” and “then”) and \(Q \cup \varSigma \cup \{H, N\}\subseteq N_C\) (the latter two for “halt” and “not-head”).

The idea is to construct a set of GCIs that encodes the transition function \(\delta\) of M such that a model should be a structure like the one shown in Fig. 2, which corresponds to the unique run of the machine started with the initial state \(q_0\) on the empty tape (where \(x_{i,j}\) is the letter at position j at step i of the run, and \(q_{i,j}\) is either N, if the head is not at position j at step i, or the state of the machine at step i otherwise).

More formally, the TBox \({\mathcal{T}} _M\) consists of the global RVM \(tr\sqsubseteq rt\) together with the following GCIs, whose rôle will be explained later: Intuitively, these GCIs have the following meaning:The following lemma shows the correctness of the reduction, and thus yields the undecidability result stated in Theorem 4.

Using the fact that GCIs and local RVMs can express global RVMs, or the trick employed in the proof of Corollary 2, we can transfer the undecidability result stated in Theorem 4 also to local RVMs and TBoxes of a restricted form.

In this paper we have, on the one hand, given a more direct proof of the known fact that subsumption in \(\mathcal{FL}_0\) w.r.t. GCIs is ExpTime-hard. We believe that the ideas underlying the reduction employed in this proof may turn out to be helpful for showing ExpTime-hardness for other inexpressive DLs. On the other hand, we have determined decidable and undecidable cases for \(\mathcal{FL}_0\) extended with role-value maps. For the case without a TBox, we have shown that admissible global RVMs leave the subsumption problem decidable. What remains open is the question whether the same is true for admissible local RVMs. For the decidable cases, it would also be interesting to investigate the complexity of the subsumption problem, depending on the form of the available RVMs.