In this paper syntactic objects|concept constructors called part restrictions which realize rational grading are considered in Description Logics (DLs). Being able to convey statements about a rational part of a set of successors, part restrictions essentially enrich the expressive capabilities of DLs. We examine an extension of well-studied DL ALCQIHR+ with part restrictions, and prove that the reasoning in the extended logic is still decidable. The proof uses tableaux technique augmented with indices technique, designed for dealing with part restrictions.
Description Logics (DLs) are widely used in knowledge-based systems. The
representation in the language of transitive relations, in di erent possible ways [
Inverse roles enable the language to describe both the whole by means of
its components and vice versa, for example has part and is part of. This syntax
extension is captured in DL ALCIHR+ [
We go further considering concept constructors which we call part
restrictions, capable of distinguishing a rational part of a set of successors. These
constructors are analogues of the modal operators for rational grading [
On the other hand, presburger constraints in the language of extended modal
logic EXML [
A combinatorial approach to grading in modal logics [
Nonetheless, the use of separate rational grading, having its place also in
modal logics, proves markedly bene cial in DLs. Part restrictions can be
combined in a DL with many other constructors. Indices technique, specially designed
for exploring the part restrictions, allows following a common way for obtaining
decidability and complexity results as in less, so in more expressive languages
with rational grading. In particular, reasoning complexity results|polynomial,
NP, and co-NP|concerning a range of description logics from the AL-family
with part restrictions added, are obtained ([
Now we consider the DL ALCQPIHR+ , in which the language of ALCQIHR+ is augmented with part restrictions. We use the tableaux technique to prove that the reasoning in the extended logic is also decidable. 2
The ALCQPIHR+ -syntax and semantics di er from those of ALCQIHR+ only in the presence of part restrictions.
De nition 1. Let Co 6= ; be a set of concept names, Ro 6= ; be a set of role names, some of which transitive, and Q0 be a set of rational numbers in (0; 1). We denote the set of transitive role names R+, so that R+ Ro. Then we de ne the set of ALCQPIHR+ -roles (we will refer to simply as `roles') as R = Ro [ fR j R 2 Rog, where R is the inverse role of R.
As the inverse relation on roles is symmetric, to avoid considering roles such as R we de ne a function Inv which returns the inverse of a role. Formally, Inv(R) = R , if R is a role name, and Inv(R ) = R. Thus, Inv(Inv(R)) = R.
A role inclusion axiom has the form R v S, for two roles R and S, and the acyclic inclusion relation v. For a set of role inclusion axioms R, a role hierarchy is R+ := R [ fInv(R) v Inv(S) j R v S 2 Rg; v+ , where v+ is the re exive and transitive closure of v over R [ fInv(R) v Inv(S) j R v S 2 Rg.
A role R is simple with respect to R+ i R 62 R+ and, for any S v+R; S is also simple w.r.t. R+.
The set of ALCQPIHR+-concepts (we will refer to simply as `concepts') is the smallest set such that: 1. every concept name is a concept; 2. if C and D are concepts, and R is a role, then :C; C u D; C t D; 8R:C, and 9R:C are concepts; 3. if C is a concept, R is a simple role, n 0, and r 2 Q0, then > nR:C; 6 nR:C; M rR:C, and W rR:C are concepts.
The limitation roles in qualifying number restrictions, as well as in part
restrictions to be simple is used essentially in the proofs. From the other side, the
presence in the language of role hierarchies together with only number
restrictions on transitive roles leads to undecidability [
An interpretation I = ( I ; I ) consisting of a nonempty set I , called the domain of I, and a function I which maps every concept to a subset of I and every role to a subset of I I , is de ned in a standard way.1 We only set the additional restriction for any object x 2 I and any role R 2 R the set of objects, RI -related to (RI -neighbours of) x, denoted RI (x), to be nite. RI (x; C) denotes the set fy j hx; yi 2 RI and y 2 CI g of RI -neighbours of x which are in CI , and ]M denotes the cardinality of a set M . For part restrictions, for any concept C, simple role R, and r 2 Q0 the de nitions of mapping are: (M rR:C)I = fx 2
I j ]RI (x; C) > r:]RI (x)g (W rR:C)I = fx 2
I j ]RI (x; :C) r:]RI (x)g = (:M rR::C)I
An interpretation I satis es a role hierarchy R+ i RI SI for any R v+ S 2 R+; we denote that by I j= R+.
A concept C is satis able with respect to a role hierarchy R+ i there exists an interpretation I such that I j= R+ and CI 6= ;. Such an interpretation is called a model of C with respect to R+. For an object x 2 CI we say that x satis es C, also that x is an instance of C, while x 2 I nCI refuses C.
Thus, for x 2 I ; x is in (M rR:C)I i strictly greater than r part of RI neighbours of x satis es C, and x is in (W rR:C)I i no greater than r part of RI -neighbours of x refuses C.
A concept D subsumes a concept C with respect to R+ (denoted C vR+D) i CI DI holds for every interpretation I such that I j= R+.
Checking the subsumption between concepts is the most general reasoning
task in DLs. From the other side, C v D i C u :D is unsatis able. Thus, in
1 All de nitions and techniques from Section 5 of [
In what follows we consider concepts to be in the negation normal form (NNF). We denote the NNF of :C by C. The NNF of M rR:C is W rR::C, and, dually, W rR:C = M rR::C. For any concept C in NNF we denote with clos(C) the smallest set of concepts containing C and closed under sub-concepts and . The size of clos(C) is linear to the size of C. With RC we denote the set of roles occurring in C and their inverses. 3
We will use a tableaux algorithm to test the satis ability of a concept. We extend the de nition of ALCQIHR+ -tableau by modifying one property to re ect the presence of part restrictions, and adding two new ones. Thus we obtain a de nition of a tableau for ALCQPIHR+ .
De nition 2. A tableau T for a concept D in NNF with respect to a role hierarchy R+ is a triple (S; L; E ), where S is a set of individuals, L : S ! 2clos(D) is a function mapping each individual of S to a set of concepts which is a subset of clos(D), E : RD ! 2S S is a function mapping each role occurring in RD to a set of pairs of individuals, and there is some individual s 2 S such that D 2 L(s). For all individuals s; t 2 S, concepts in clos(D), and roles in RD, T must satisfy 13 properties.
We denote with RT (s) the set of individuals, R-related to s, and RT (s; C) := ft 2 S j hs; ti 2 E (R) and C 2 L(t)g. The new and the modi ed properties follow. In property 13 (modi ed property 11 from the de nition of ALCQIHR+ tableau), and in what follows, is a placeholder, besides for > n and 6 n, for arbitrary n 0, also for 9, and for M r and W r, for arbitrary r 2 Q0. 11: If M rR:C 2 L(s); then ]RT (s; C) > r:]RT (s): 12: If W rR:C 2 L(s); then ]RT (s;
C) r:]RT (s): 13: If
R:C 2 L(s) and hs; ti 2 E (R); then C 2 L(t) or C 2 L(t):
Having the de nition of ALCQPIHR+ -tableau, we can prove Lemma 1 following the standard way, also for the new and modi ed properties. Lemma 1. An ALCQPIHR+ -concept D is satis able with respect to a role hierarchy R+ i there exists a tableau for D with respect to R+. 4
Lemma 1 guarantees that the algorithm constructing tableaux for ALCQPIHR+ concepts can serve as a decision procedure for concept satis ability (and hence, also for subsumption between concepts) with respect to a role hierarchy R+. We present such an algorithm.
As usual with the tableaux algorithms, ALCQPIHR+ -algorithm tries to prove the satis ability of a concept D by constructing a completion tree (c.t. for short) T, from which a tableau for D can be build. Each node x of the tree is labelled with a set of concepts L(x) which is a subset of clos(D), and each edge hx; yi is labelled with a set of roles L(hx; yi) which is a subset of RD. The algorithm starts with a single node (the c.t. root) x0 with L(x0) = fDg, and the tree is then expanded by completion rules, which decompose the concepts in the nodes' labels, and add new nodes and edges, giving the relationships between nodes, and new labels to the nodes and edges.
A node y is an R-successor of a node x if y is a successor of x and S 2 L(hx; yi) for some S with S v+ R; y is an R-neighbour of x if it is an R-successor of x, or if x is an Inv(R)-successor of y.
We denote with RT(x) the set of R-neighbours of a node x in the c.t. T, and with RT(x; C)|the set of R-neighbours of x in T which are labelled with C.
A c.t. T is said to contain a clash (i.e., the obvious contradiction) if, for some node x in T, a concept C, a role R, some n 0, and some r 2 Q0 any of the following is the case. Otherwise it is clash-free.
CL1: fC; :Cg L(x) CL2: 6 nR:C 2 L(x) and ]RT(x; C) > n CL3: M rR:C 2 L(x) and ]RT(x; C)
r:]RT(x)
CL4: W rR:C 2 L(x) and ]RT(x; :C) > r:]RT(x)
A completion tree is complete if none of the completion rules is applicable, or if, for some node x, L(x) contains a clash of type CL1 or type CL2.2
If, for a concept D, the completion rules can be applied in a way to yield a complete and clash-free completion tree, then the algorithm returns `D is satisable'; otherwise, it returns `D is unsatis able'.
During the expansion the algorithm uses the pair-wise blocking technique as
de ned in [
Figure 1 presents the completion rules which are new or modi ed in comparison with ones in the ALCQIHR+ -algorithm. choose-rule is augmented (via the placeholder ) to add also labels, induced by 9-concepts and part restrictions.
In the presence of part restrictions, >-rule which adds all the necessary successors at ones leads to incompleteness.3 So, it is modi ed to add successors one by one, thus preventing the occurrence of redundant neighbours. This needs
CL4 (which are also conditions for applicability of M -rule and W -rule, see Figure 1) can appear and disappear dynamically during the c.t. generation. That is why we exclude them from the de nition of the c.t. completeness. 3 For example, the concept Au9R : > 4R:>u 6 5R:>uM 25 R:(:A)uW 21 R:A , where > = A t :A, and A is a concept name, has a unique tableau (modulo labelling of the individuals) with just four individuals. But no complete and clash-free c.t. can be built from that tableau using the `all-at-once' >-rule. some modi cation of 6-rule also. 6-rule transfers the label of an edge to just one other edge. So, the use of L(hx; yi) \ L(hx; zi) = ; condition in the rule is justi ed as follows. If two edges are labelled with the same role, it has been labelling initially (even if some label transfer has happened meanwhile) two different edges connecting x with two of its neighbours. The possible cases are: 1) the labels of y and z are di erent and contradict each other for any labelling by choose-rule, so y and z cannot be merged; 2) the labels of y and z are di erent but there is a labelling by choose-rule which makes them not contradicting, then there is no need nodes to be merged, as when this labelling is made to the rstly generated node, the second one would not be generated at all; 3) the labels of y and z are identical, then the generation of both nodes is triggered by >n-concept with n 2, M -, or W -concept, or, anyway, they are used for the satisfying in the c.t. of such a concept, so they must not be merged.
M -rule and W -rule (the part rules ) are new generating rules (in addition to
9-rule and >-rule) which deal with part restrictions. The rest of the rules|u-,
t-, 9-, 8-, and 8+-rule|remain just as they are in [
If 1. R:C 2 L(x), x is not indirectly blocked, and
2. there is an R-neighbour y of x with fC; Cg \ L(y) = ; then L(y) ! L(y) [ fEg for some E 2 fC; Cg If 1. > nR:C 2 L(x), x is not blocked, and
2. ]RT(x; C) < n then create a new successor y of x with L(hx; yi) = fRg and L(y) = fCg If 1. 6 nR:C 2 L(x), x is not indirectly blocked, and
C 2 L(y), C 2 L(z), L(hx; yi) \ L(hx; zi) = ;, and y is not a predecessor of x then 1. L(z) ! L(z) [ L(y), 2. If z is a predecessor of x then L(hz; xi) ! L(hz; xi) [ fInv(S)jS 2 L(hx; yi)g else L(hx; zi) ! L(hx; zi) [ L(hx; yi) 3. L(hx; yi) ! ; If 1. M rR:C 2 L(x), x is not blocked, and 2. ]RT(x; C) r:]RT(x) then calculate BANx, and if 3. ]RT(x) < BANx then create a new successor y of x with L(hx; yi) = fRg and L(y) = fCg If 1. W rR:C 2 L(x), x is not blocked, and 2. ]RT(x; C) > r:]RT(x) then calculate BANx, and if 3. ]RT(x) < BANx then create a new successor y of x with L(hx; yi) = fRg and L(y) = fCg
We impose a rule application strategy : any generating rule can be applied only if all non-generating rules (i.e., u-, t-, 8-, 8+-, choose- and 6-rule) are inapplicable. Anyway, the generation process is non-deterministic in both which rule (from the group of non-generating or generating ones) to be applied, and which concept(s) to be chosen in the non-deterministic t-, choose-, and 6-rule.
The rule application strategy is essential for the successful `work' of 6-rule, and for the part rules. It ensures that a) all concepts `talking' about neighbours are already present in L(x), and b) all possible (re)labelling of neighbours of x is done before the application of a part rule. Both are necessary for applying the indices technique for the correct generation of successors, caused by part restrictions. The check-up in part rules (in 3.) for not reaching the border amount of neighbours for the current node x (BANx) is a kind of `horizontal blocking' of the generation process, used to ensure inapplicability of part rules after a given moment. The notion is crucial for the termination of the algorithm, and its use is based on Lemma 6, which is the upshot of the indices technique. 5
We develop a speci c technique, which we call indices technique, to cope with the presence of part restrictions. This technique permits to extend appropriately the de nition of a clash, to design completion rules, dealing with part restriction, and to give an adequate rule application strategy, as they are presented in the previous section, all to guarantee the correctness of the tableaux algorithm. 5.1
The clashes with part restrictions CL3 and CL4, which are also conditions for applicability of part rules, are dynamic. Applied consecutively, part rules can `repair' one clash, and, at the same time, provoke another. Thus, instances of CL3 and CL4 can appear and disappear, in some cases in nitely, during the c.t. generation, even if the initial concept is satis able. So, we have to take special care both to ensure the termination of part rules application, and not to leave avoidable `part' clashes in the completion tree. That turns out to be the main di culty in designing the algorithm. We overcome it by proving that if it is possible to unfold part restrictions at a given node avoiding simultaneously both kinds of clashes, it can be done within some number of neighbours. As clashes are always connected with a single node, talking about its label and its neighbours, that is enough to guarantee the termination. The following subsection presents the technique in details. 5.2
Counteracting part restrictions. Clusters We start our analysis with the simplest case when, for a node x of the c.t. T, there are in L(x) only part restrictions, and they all are with the same role R, and with sub-concepts which are either a xed concept C, or its negation C, and x is not an Inv(R)-successor. All such part restrictions form the set:
C; W r3R:C; W r4R: (1) fM r1R:C; M r2R: Cg
We call the subset of (1) which is in L(x) a cluster of R and C at x in T, and we denote it ClxT(R; C). It is obvious, that during the generation of (R-) successors of x (if it is necessary) instances of CL3 and CL4 can appear only if two contradicting part restrictions are in that cluster.
De nition 3. A part restriction which is in the label of a node x in a c.t. T is T-satis ed (at x) if there is no clash with it at x.
A cluster is T-satis ed if all part restrictions in it are T-satis ed.
A part restriction (a cluster) is c.t.-satis able if it can be T-satis ed, for some c.t. T.
In fact, in (1) there can be more than one part restriction of any of the four types. But note that, if M rR:C is T-satis ed, then that is the case with M r0R:C (being in the label of the same node), for any r0 < r. So, we can take r1 and r2 to be the maximums, and, by analogues reasons, r3 and r4 to be the minimums of the r-s in part restrictions of the corresponding types. Thus we obtain the upper, representative for the c.t.-satis ability of all part restrictions in the node's label, set with only four ones.
The idea behind the c.t.-satis ability is that if a cluster, and more general, the set of all part restrictions labelling a node, is c.t.-satis able, then a c.t. without clashes with part restrictions at that node can be non-deterministically generated, while the part rules become inapplicable for this node (as the inequality in condition 2 or 3 in part rules becomes false). So, concerning part restrictions, c.t.-satis ability is a su cient condition for obtaining a clash-free complete c.t.
Our next observation is that both M r1R:C and W r3R:C act in the same direction concerning c.t. generation, as the former forces the addition of enough Rsuccessors of x labelled with C, and the latter limits the number of R-successors of x labelled with C. The same holds for M r2R: C and W r4R: C with respect to C. At that time, as M r1R:C, so W r3R:C counteract with any of M r2R: C and W r4R: C. This leads to two main possibilities for ClxT(R; C):
A. The cluster contains only part restrictions, acting in the same direction (or just a single one)|we call it cluster of type A, or A-cluster. In the absence of counteracting part restrictions these clusters are always c.t.-satis able.
B. The cluster contains at least two counteracting part restrictions|we call it cluster of type B, or B-cluster.
In order the c.t. generation process to be able to c.t.-satisfy a B-cluster, and to avoid CL3 and CL4 clashes, the next inequalities between the r-s in the cluster (or between the indices, from where we take the name of indices technique) must be ful lled|follows directly from the semantics of part restrictions, the above remarks about counteractions, and the de nition of c.t.-satis ability: 1 r1 + r2 < 1 4 r3 + r4 1, what is 2 r1 < r4 (a) r3 + r4 > 1, or 3 r2 < r3 (b) r3 + r4 = 1
If any of the inequalities 1 {4 does not hold, any complete c.t. will contain a clash, as it is impossible to c.t.-satisfy simultaneously (at the same node) the part restrictions in which are the indices, taking part in the failed inequality.
We can combine that four inequalities in just one taking into account the kind of interaction between part restrictions. W r3R:C means that C has to label not greater than r3 part of all R-neighbours of x, i.e., that C has to label at least (1 r3) part of them. We set r = max fr1; 1 r3g (or, if the part restriction with r1 or r3 is not in the cluster, r is just the expression with the other). Now, it is obvious that if C labels greater than r part of all R-neighbours of x, then both M r1R:C and W r3R:C are (or the single one from the couple which is in the cluster, is) c.t.-satis ed. Analogues reasonings go with the other couple of part restrictions, acting in the same direction (the ones with M r2 and W r4), and (a part smaller than) r^ = min f1 r2; r4g .
We call dominating the part restrictions which determine r and r^.
It is important to note that r3 + r4 = 1 does not spoil the c.t.-satis ability (unlike r1 + r2 = 1). We exclude that case from the general examination, as a special sub-case, and discuss it separately. Thus, B divides into two sub-cases: B(a). The cluster contains no counteracting W part restrictions, or r3 + r4 6= 1. B(b). The cluster contains counteracting W part restrictions and r3 + r4 = 1. Clusters of type B(a). Our rst claim is: Lemma 2. For a B(a)-cluster ClxT(R; C), the inequalities 1 , 2 , 3 , and 4 (a), with the corresponding part restrictions being in the cluster, hold i r < r^. Corollary 1. r < r^ is a necessary condition for the c.t.-satis ability of a B(a)cluster ClxT(R; C).
The upper inequality is also a su cient condition for a cluster's c.t.-satis ability. Indeed, if r < r^, and the number of R-neighbours of x labelled with C| jRT(x; C)j|is strongly (due to the strong inequality for M ) between r:jRT(x)j and r^:jRT(x)j, then the dominating part restrictions are c.t.-satis ed, and so are the rest of the part restrictions in the cluster, if any. This shows that r < r^ guarantees the c.t.-satis ability; practical c.t.-satisfaction of a cluster depends on the number of neighbours, and, of course, their appropriate labelling.
Note also that even though r < r^ holds, we can have instable c.t.-satisfaction, as it can be seen from the next example. Let the dominating part restrictions be M 32 R:C and M 14 R: C. They can be T-satis ed if RT(x) has 10 nodes (with C labelling 7, and C|3 of them), and also 11 nodes (with labelling C : C| 8 : 3), while if RT(x) has 12 nodes, there is no way these part restrictions to be T-satis ed, as the rst wants C to label at least 9, and the second| C to label at least 4 R-neighbours of x. In case of 13 R-neighbours of x the part restrictions again can be simultaneously T-satis ed.
De nition 4. A cluster ClxT(R; C) is n-satis able, where n 0, if it can be c.t.-satis ed when x has exactly n R-neighbours.
A cluster is stably n-satis able, if it is n-satis able, and for any natural number n0 > n it is also n0-satis able.
A cluster is stably c.t.-satis able, if it is stably n-satis able for some n 0.
Note that from the above de nition it follows that if a cluster is stably nsatis able, it is also stably n0-satis able, for any natural number n0 > n.
In the example above the cluster is 10-, and 11-satis able, it is not 12satis able, and it is (in fact|stably) 13-satis able.
So, if we have a su cient condition for stable n-satis ability of B(a)-clusters, we will know exactly when, in the non-deterministic c.t. generation process, stable c.t.-satisfaction of such a cluster will be achieved in at least one nondeterministic generation (we call it a successful generation). Then we will be able to key at that moment the part rules with respect to the part restrictions of that cluster, thus avoiding in nite rules application in the unsuccessful generations. Lemma 3. Let, for a B(a)-cluster ClxT(R; C), r < r^ hold. Then a su cient condition for the non-deterministic jRT(x)j-satis ability of the cluster is: jRT(x)j > r^1 r (]) Lemma 4. Let, for a B(a)-cluster ClxT(R; C), r < r^ and (]) hold, and the dominating part restrictions in the cluster be T-satis ed. Then any generating rule can always be applied in a way to yield T0 such that the cluster to be T0satis ed.
Lemma 4 shows that (]) also guarantees the stability of the non-deterministic c.t.-satis ability, namely stable r^1 r + 1 -satis ability. Being once ful lled, (]) holds for any greater number of R-neighbours of x, and so c.t.-satisfying of the dominating part restrictions can be preserved as RT(x) grows.
Thus, Lemma 3 and Lemma 4 guarantee for a c.t.-satis able (with r < r^) B(a)-cluster ClxT(R; C) that, having the number of R-neighbours of x equal to, or greater than r^1 r + 1 (what we will call the border amount of neighbours of x; BANx, for that cluster), the cluster can be non-deterministically c.t.-satis ed. Then, the termination of application of rules, triggered by (the part restrictions in) that cluster, is ensured by the check-up for jRT(x)j.
Shortly said, any c.t.-satis able B(a)-cluster can be non-deterministically stably c.t.-satis ed when the node has enough many neighbours on the role in the cluster. We will rate that in the general case for all (possibly counteracting) part restrictions, to preserve from in nite application of part rules. Clusters of type B(b). B(b)-clusters are determined by the equality 4 (b) r3+r4 = 1 for the indices in W part restrictions. These clusters are c.t.-satis able if 2 r1 < r4 and 3 r2 < r3 hold (in case that the corresponding M part restrictions are in the cluster; in that case 1 obviously also holds). Thus, if 2 and 3 hold, or some M part restriction is missing, 4 (b) can be considered as a su cient condition for the c.t.-satis ability of a B(b)-cluster.
Lemma 5. Let, for a B(b)-cluster ClxT(R; C), r1 < r4 and r2 < r3 hold, in case the corresponding M part restrictions are in the cluster. Then the cluster is c.t.-satis able, and the su cient condition it to be non-deterministically c.t.satis ed is the number of R-neighbours of x to be devisable by the denominator of r3 and r4.
The general case. Let us recall that the application of a part rule requires all possible applications of non-generating rules for the current node to be already done, what ensures all possible (at the moment) concepts, including part restrictions, to be already present in the node's label. Generalizing the considerations for counteracting in clusters, also taking into account the other concepts, triggering generating rules, and using the indices technique, we prove: Lemma 6. Let x be a node of a completion tree T, and let all possible applications of non-generating rules for x be done. Then it can be calculated a natural number BANx 1, depending on the concepts in L(x), and if x is a successor of u, possibly also depending on the concepts in L(u), and having the following property: all part restrictions in L(x) which are simultaneously T-satis able can be non-deterministically simultaneously T-satis ed when the number of neighbours of x on any role at the uppermost level in these part restrictions becomes equal to BANx.
Lemma 6 both legitimates the use of BANx in the part rules applicability check-up, thus ensuring termination, and guarantees that all simultaneously c.t.-satis able part restrictions will be non-deterministically c.t.-satis ed, so that there would not be clashes with them in the complete c.t.
Note that the border amount of neighbours can change only if L(x) or L(u) be changed, for example by adding of some concept to any of them caused by an application of a rule for a successor. As the number of such possible changes is limited by the number of concepts in clos(D), after nite number of recalculations we will obtain the nal for the node x BANx. 6
As usual with tableaux algorithms we prove lemmas that the algorithm
always terminates, and that it is sound and complete. The termination is ensured
by pair-wise blocking, and by BAN -checkup which guarantees nite (at most
exponential|in case of the usual binary coding of numbers) branching at a node.
The build of a tableau from the completion tree and the reverse follows the
constructions from [
DL ALCQPIHR+ augments ALCQIHR+ with the ability to express rational grading. We showed that the decision procedure for the latter logic can be naturally extended to capture the new one. This indicates that the approach which realizes rational grading independently from integer grading is fruitful, and can be applied even to expressive description logics to give in a convenient way their rational grading extensions, still keeping the decidability.
Acknowledgments We would like to thank the anonymous reviewers for their valuable questions, remarks and suggestions. Unpublished Abstracts, CiE 2014, pages 261{270, Budapest, Hungary, 2014. Available online at https://www.fmi.uni-sofia.bg/about/lio/yanchev/ct_cie2014. 18. M. Yanchev. PSPACE reasoning in an expressive description logic with rational grading. In Proceedings, 11th Panhellenic Logic Symposium, pages 102{107, Delphi, Greece, 2017. 19. M. Yanchev. Decidability of an expressive description logic with rational grading, 2019. arXiv:1905.10338 [cs.LO].