the rough DL ℰℒ⊥ subsumption. Rough logics, vagueness, subsumption
Rough description logics extend usual description logics by concept operators that use rough sets to add a qualitative form of vagueness to concepts. In the field of rough sets, the domain is partitioned by an equivalence relation, the so-called the indiscernibility relation , that groups indistinguishable elements into equivalence classes, also known as granules. Based on this partition, each set is associated with two additional sets. One is the lower approximation , which contains all elements whose equivalence class is completely contained in . The second set is the upper approximation , which contains all those elements that belong to an equivalence class that has an overlap with . When applied to concepts, the lower approximation models the “strong” or typical instances of , while the upper approximation models elements that are at least “close” or similar to instances of .
Rough description logics have been defined as extensions of several classical DLs ranging from
ℰℒ to ℒ. Reasoning in those rough DLs has mostly been investigated in relation to subsumption
[
Already rough sets alone have been used to structure data early on [
In more general settings, clustering algorithms are a prime means to structure data as these algorithms
group data items according to their homogeneity or proximity into clusters. There is a plethora of
such methods and corresponding implementations readily available. A common and well-used type of
clustering methods are the hierarchical clustering methods like the classical COBWEB algorithm [
CEUR
ceur-ws.org and its variants. These clustering algorithms partition the data and efectively construct a dendrogram of the data; i.e., they result in a hierarchy of clusters. The corresponding partitions are then a linearly ordered set of equivalence relations.
The hierarchy of partitions obtained from hierarchical clustering or from indiscernibility relations
motivates the extension of rough DLs by a finite, linearly ordered set of equivalence relations (being
used as indiscernibility relations) 1, . . . , . The results of clustering the data can be incorporated in
the knowledge base by augmenting the ABox with the role assertions for pairs from the same cluster, i.e.,
from pairs related by . Such an augmentation of the ABox could be achieved by a mapping commonly
used in ontology-based data access (OBDA) [
(originally introduced in [
/ linwhich uses a finite, linearly ordered set of indiscernibility tion by one indiscernibility relation, to ℰℒ⊥ / lin, we relations, and as such admits the use of a hierarchy of granulations. In this initial study on ℰℒ⊥ / linand develop a decision procedure based on a completion algorithm investigate subsumption in ℰℒ⊥
/ linTBoxes. This algorithm serves as a starting point that essentially computes canonical models for ℰℒ⊥ for investigating ABox reasoning tasks for this logic. The paper is organised as follows: in the next / lin. In Section 3 we develop the reasoning algorithm based on a section we introduce the rough DL ℰℒ⊥ normal form and completion rules. In Section 4 we supply a brief discussion on possible extensions and we end the paper with conclusion and an outlook on future work.
/ lin
where several equivalence relations (representing indiscernibility at We consider an extension of ℰℒ⊥ diferent levels of detail) are used. In our setting, these relations are totally ordered from the coarsest to the most finely-grained. More formally, given ≥ 1, we consider equivalence relations ∼ 1, . . . , ∼ such that ∼ ⊆ ∼ +1 for all 1 ≤ < . That is, ∼ 1 is the most fine-grained relation, while ∼ is the coarsest. Note that ∼ partitions each equivalence class of ∼ +1 into (possibly) smaller classes.
/ linconcepts is constructed through the syntactic rule Given a fixed but arbitrary ∈ N, the set of ℰℒ⊥ ::= | ⊤ | ⊥ | ⊓ | ∃. | | where ∈ NC, ∈ NR, and 1 ≤ ≤ . Concepts of the form are called lower approximation of w.r.t. ∼ and those of the form are called upper approximation of w.r.t. ∼ . As usual, a ℰℒ⊥ / linTBox / linconcepts. (or ontology) is a finite set of GCIs of the form ⊑ , where and are ℰℒ⊥
The semantics is based on interpretations of the form ℐ = (Δℐ , · ℐ , {∼ | 1 ≤ ≤ }) where (Δℐ , · ℐ ) is a standard DL interpretation, and ∼ 1, . . . , ∼ are equivalence relations over Δℐ such that ∼ ⊆ ∼ +1 holds for all 1 ≤ < . Given an element ∈ Δℐ , we denote as [ ] the equivalence class of w.r.t. ∼ , which is the class of all objects ∈ Δℐ such that (, ) ∈ ∼ . The interpretation function is extended / linconcepts as usual for ⊤, ⊥, ⊓, and ∃, while for the lower and upper approximations, to arbitrary ℰℒ⊥ we define ( )ℐ := { ∈ Δℐ | [ ] ⊆ ℐ } and ( )ℐ := { ∈ Δℐ | [ ] ∩ ℐ ̸= ∅}.
An interpretation satisfies the GCI ⊑ (denoted as ℐ |= ⊑ ) if ℐ ⊆ ℐ . The interpretation ℐ is a model of the TBox (denoted ℐ |= ) if ℐ |= ⊑ holds for all GCIs ⊑ ∈ .
Note in particular that for every ∈ Δℐ and every , with 1 ≤ < , it holds that [ ] ⊆ [ ]+1, and hence also ( +1)ℐ ⊆ ( )ℐ ⊆ ( )ℐ ⊆ ( +1)ℐ for all concepts . The following proposition is a consequence of these properties.
Proposition 1. For all , with 1 ≤ ≤ ≤ , all concepts , and all interpretations ℐ the following equivalences hold: 1. (a) (︀ ( ) )︀ ℐ = ( )ℐ ; 4. (︀ ( ) )︀ ℐ = ( )ℐ .
Proof. We prove only the claims 1. and 3.; the other two can be shown analogously.
For Claim 1.(a), ∈ (( ) )ℐ if [ ] ⊆ ( )ℐ if (since ∼ ⊆ ∼ ) [ ] ⊆ [ ] ⊆ ℐ if ∈ ( )ℐ . Similarly for 1.(b), ∈ (( ))ℐ if [ ] ⊆ ( )ℐ if for every ∈ [ ], it holds that [ ] ⊆ ℐ if (since ∼ holds and implies that ∼ holds) [ ] ⊆ ℐ if ∈ ( )ℐ .
For Claim 3., ∈ (( ))ℐ if [ ] ∩ ( )ℐ ̸= ∅ if there exists ∈ [ ] such that ∈ ( )ℐ if there is ∈ [ ] with [ ] ⊆ ℐ if (because ∼ holds and implies that ∼ holds) [ ] ⊆ ℐ if ∈ ( )ℐ .
If = Claims 1 and 2 from Proposition 1 cover idempotence of both kinds of approximations. This afects the design of the completion rules that treat propagation within the same level of roughness, that is w.r.t. one . For < the claims from Proposition 1 indicate how information is to be propagated or absorbed between diferent levels of roughness.
Other important properties which combine the approximation concept constructors for each given
indiscernibility relation are the following, which were originally proven in [
/ linconcepts , , and all with 1 ≤ ≤ , the following properties Proposition 2. For any three ℰℒ⊥ hold: 1. |= ⊑ if |= ⊑ ; and 2. if |= ⊑ and |= ⊑ , then |= ⊑ ; and 3. if |= ⊑ and |= ⊑ , then |= ⊑ .
These properties indicate how information is to be propagated within the same level of roughness. / linin the following All of these properties will be useful when we design a reasoning algorithm for ℰℒ⊥ section.
The rough DL ℰℒ⊥ / linwhere = 1; that is, where only one equivalence is the special case of ℰℒ⊥ relation is used. Since ℰℒ⊥ is a particular case of ℰℒ⊥, where the GCIs ⊑ 1 and 1 ⊑ are satisfied / linis obviously a generalisation of the classical DL ℰℒ⊥. As usual in these logics, for all ∈ NC, ℰℒ⊥ we are mainly interested in deciding whether a consequence follows from an ontology; in this case, we consider the problem of deciding subsumption between two concept names. We say that ∈ NC is subsumed by ∈ NC w.r.t. the TBox ( |= ⊑ ) if every model of also satisfies the GCI ⊑ .
/ lin
We are interested in developing a reasoning algorithm capable of deciding subsumption relationships
/ linTBox. As this logic is an extension of ℰℒ⊥, we extend the known
between concepts w.r.t. a given ℰℒ⊥
completion algorithm [
As a first step, we need to limit the form that GCIs can take, requiring the TBox to comply with a normal form; that is, that all the axioms are of one of the forms 1 ⊓ 2 ⊑ , ⊑ ∃., ∃. ⊑ , ⊑ , ⊑ , ⊑ , where , ∈ NC ∪ {⊤}, ∈ NC ∪ {⊤, ⊥}, and 1 ≤ ≤ .1
Any TBox can be transformed into normal form applying the rules from Table 1—where NF1 uses the commutativity of conjunction—until no rule can be applied anymore. The resulting TBox is a conservative extension of which, importantly, is only polynomially larger than as it is found after only a polynomial number of rule applications.
Our completion algorithm extends the ideas introduced in [
More formally, for each ∈ NC ∪ {⊤} appearing in the normalised TBox , and for each 1 ≤ ≤ we preserve two sets called () and (). In addition, we keep track of a set () and for each role name ∈ NR appearing in a set (, ). Hence, for each such , we keep 2 + ℓ + 1 many such completion sets, where ℓ is the number of role names in . With polynomially many s in the normalised TBox, the completion algorithm uses polynomially many completion sets.
The elements of each completion set all belong to NC ∪ {⊤, ⊥}. The idea is that these sets are sound
w.r.t. subsumption relations among simple concepts. Specifically, throughout the completion algorithm,
the application of completion rules preserves the following invariants:
1. if ∈ () then |= ⊑
2. if ∈ () then |= ⊑
3. if ∈ () then |= ⊑ and
4. if ∈ (, ) then |= ⊑ ∃.
for all ∈ NC ∪ {⊤}, ∈ NC ∪ {⊤, ⊥}, ∈ NR, and 1 ≤ ≤ . These are essentially the same
in [
The completion sets are initialized with obvious tautologies; that is, at the beginning of the algorithm the sets are defined as () = () := {, ⊤}, () := {⊤}, (, ) := ∅ for all ∈ NC ∪ {⊤}, ∈ NR, 1 ≤ ≤ . Clearly this initialization preserves the invariants mentioned above. These sets are extended through application of the completion rules described in Table 2. As 1For brevity, we consider axioms of the form ⊑ as ⊤ ⊓ ⊑ . if {1, 2} ⊆ () and 1 ⊓ 2 ⊑ ∈ , then add to () if ∈ () and ⊑ ∃. ∈ , then add to (, ) if ∈ (, ), ∈ () and ∃. ⊑ ∈ , then add to () if {1, 2} ∈ () and 1 ⊓ 2 ⊑ ∈ , then add to () if 1 ∈ (), 2 ∈ () and 1 ⊓ 2 ⊑ ∈ , then add to () if ∈ () and ⊑ ∈ , then add to () if ∈ () and ⊑ ∈ , then add to () if ∈ () and ⊑ ∈ , then add to () if ∈ (), then add to () cr10 if ∈ (), then add to () cr11 if ∈ () and < , then add to () cr12 if ∈ () and < , then add to () cr13 cr14 if ∈ () and ∈ (), then add to () if ∈ () and ∈ (), then add to () cr15 if ∈ () and ∈ (), then add to () cr18 if ⊥ ∈ (), then add ⊥ to () cr16 if ∈ (, ) and ⊥ ∈ (), then add ⊥ to () cr17
if ∈ () and ⊥ ∈ (), then add ⊥ to () usual for these kinds of algorithms, the rules are only applied if they add an element to one of the sets involved; that is, if the concept to be added is not already present in the set. The completion algorithm applies rules until no rule is applicable anymore; at that point, we say that the algorithm is saturated.
Note that this algorithm becomes saturated after at most polynomially many rule applications (in and the size of ). Indeed, there are (2 + ℓ + 1) sets, where ℓ is the number of role names in and is the number of concept names in . Each of this sets contains at most + 2 elements (the concept names in plus ⊤ and ⊥). Since each rule application adds one element to one of the sets, at most (2 + ℓ + 1)( + 2) rule applications are needed before reaching saturation. In addition, the conditions for the application of a rule require only a lookup between the sets and the GCIs in , which can also be performed in polynomial time. Thus, overall the algorithm needs only polynomial time to be saturated.
The result of the completion algorithm can be used to decide all the atomic subsumption relations entailed by the TBox . That is, for every , ∈ NC we get that |= ⊑ if ∈ (). Soundness is a consequence of the invariants described above.
Lemma 3. The completion algorithm preserves the four invariants, throughout all rule applications. Proof. The proof is by induction on rule applications. The induction base is satisfied by the initialization. For rules without rough constructors (cr1-cr3 and cr16) soundness was shown already in [15].
For rules cr6 to cr15, cr17, and cr18 soundness is a consequence of Propositions 1 and 2. Since the rules cr11 and cr12 treat the interaction of diferent indiscernibility relations, we give a detailed proof of them. For cr11, suppose |= ⊑ and < . For every model ℐ and every ∈ Δℐ , if ∈ ℐ , then ∈ ℐ and thus [ ] ⊆ ℐ . Since from < follows that [ ] ⊆ [ ] , we obtain [ ] ⊆ ℐ holds and thus ∈ ℐ . This implies |= ⊑ . The proof for cr12 is analogous.
The only remaining rules are cr4 and cr5. For the rule cr4, suppose that |= ⊑ 1 and ⊑ ⊑ ⊑ ⊑ ⊑ ⊑ ∼ ∼ , , ∼ ∼ |= ⊑ 2 . For every model ℐ and every ∈ Δℐ , if ∈ ℐ then [ ] ⊆ 1ℐ ∩ 2ℐ and hence (as ℐ |= 1 ⊓ 2 ⊑ ) [ ] ⊆ ℐ , which implies |= ⊑ . Rule cr5 can be treated analogously.
For the converse direction—completeness—we follow the usual approach of building a sort of canonical model of that serves as a counterexample for all the atomic subsumption relations which do not appear explicitly in the generated sets. The domain Δℐ of the canonical model is composed of three kinds of elements. First, as usual for the ℰℒ family of DLs, it includes one domain element for each satisfiable concept name appearing in , which stands for a standard instance representing that concept; i.e., it is a minimal representative of . Hence, it will belong to each concept that subsumes w.r.t. . The two other kinds of domain elements handle the lower and upper approximations of named concepts in the interpretation domain. For the lower approximation, we include, for each ∼ , with 1 ≤ ≤ , an element ∼ that belongs to all concepts such that |= ⊑ . In other words, ∼ keeps information about all the concept names such that all objects indiscernible from instances of are necessarily in .
Dealing with the upper approximations requires a more nuanced construction, as a single element cannot fully witness the existence of indiscernible elements belonging to diferent concepts. We handle this with the help of diferent objects. Specifically, for each concept name such that |= ⊑ , we create an element ∼ which is a representative instance of (i.e., belongs to and all its subsumers), but exists only through its connection to the representative of . To handle the indiscernibility relations, these elements , ∼ , and ∼ all belong to the same ∼ -equivalence class. As this is not a trivial structure, we explain it in more detail here. Note that |= ⊑ means that every element of must be associated (via ∼ ) with some element of . In particular, the representative of must have such an association as well. But we cannot connect to the representative of because the symmetry of ∼ would then entail that ⊑ , which is not necessarily a consequence of . We can also not choose only one representative, as we did for the lower approximations, because (again) we cannot guarantee that the representative belongs to other concepts that are not known subsumers of . Figure 1 describes this intuition graphically. Each gray box is an equivalence class for ∼ . There can be more elements than those shown, in each class, but the figure zooms into some relevant elements of []∼ , given by tOhne tdheeriovtahtieornhsasnhdo,wsinncaet theislesfutbosfutmhee dfigubrye.Si,nce, and⊑,w,tehecroebajteectthe∼ t h rbeeeloonbgjescttos th∼ec,on∼ce ,patnd.
∼ , respectively. Importantly, these objects belong to the concepts , , and (respectively), but not to []∼ , []∼ , or []∼ , represented as the three boxes on the right.
Before formalising this construction, we recall that ⊥ requires a special treatment when it appears as a subsumer of a concept name. If |= ⊑ ⊥, we know that every model makes empty, and hence is subsumed by all concepts. Rather than making all these relations explicit, we simply handle this special case separately. / linTBox , and () the set Lemma 4. Let , be two concept names appearing in the normalised ℰℒ⊥ obtained after saturation of the completion algorithm. If {, ⊥} ∩ () = ∅, then ̸|= ⊑ . Proof. We build a model ℐ of such that ℐ ̸⊆ ℐ . The domain of this interpretation is Δℐ := {, ∼ , ∼ | 1 ≤ ≤ , and , are concept names appearing in }.
For each , with 1 ≤ ≤ , the equivalence relation ∼ is the transitive, symmetric, and reflexive closure of the relation
{(, ∼ ), (, ∼ ) | , are concept names appearing in }.
Note that all objects in Δℐ are of the form , ∼ , or ∼ . By the definition of the equivalence relations ∼ , for every ∈ Δℐ there exists some concept name such that ∼ . In particular, this means that every equivalence class of ∼ contains at least one concept name or, in other terms, that for every ∈ Δℐ there exists some ∈ NC such that [ ] = [].
To define the interpretation function · ℐ , we set for each concept name appearing in ℐ := { | ∈ ()} ∪ {∼ | ∈ ()} ∪ {∼ | ∈ (), ∈ ()} ∪ {∼ | ∈ (), ∈ NC} and for each role name ℐ := {(, ) | ∈ (, )} ∪ {(∼ , ) | ∈ (, ), ∈ ()} ∪ {(∼ , ) | ∈ (, ), ∈ ()} ∪ {(∼ , ) | ∈ (, ), ∈ (), ∈ NC}. [ ] ∩ ℐ ̸= ∅, and hence ∈ ()ℐ .
By construction ∈ ℐ and since ∈/ () we know that ∈/ ℐ . It remains to show that this is indeed a model of . This is shown through a case distinction over the possible types of axioms admitted in the normal form. We show only the cases involving rough constructors. [Case ⊑ ] If ∈ ( )ℐ , then by definition [ ] ⊆ ℐ . Let ∈ NC be such that [ ] = []. Then ∼ ∈ ℐ and hence ∈ (). As the algorithm has finished, the rule cr6 is not applicable, this means that ∈ () and by cr9 ∈ (). Consider now an arbitrary ∼ ∈ []. Since ∈ (), by construction we know that ∼ ∈ ℐ . Overall, this means that ∈ [] ⊆ ℐ , which proves the result. [Case ⊑ ] If ∈ ℐ and [ ] = []∼ for some ∈ NC, then by the rules cr9, cr10, and cr14 it follows that ∈ () which, by rule cr7 implies that ∈ () ⊆ () ⊆ (). Then, [ ] = [] ⊆ ℐ ; that is, ∈ ()ℐ . [Case ⊑ ] As in the previous case, if ∈ ℐ with [ ] = [], then ∈ (). Rule cr8 then implies that ∈ () and hence ∼ ∈ ℐ . By construction, ∼ ∈ [ ], which implies that
Thus we have a decision procedure for subsumption in ℰℒ⊥. Overall, we get the main result from this paper. / linTBoxes can be decided in polynomial time.
Theorem 5. Subsumption between concept names w.r.t. ℰℒ⊥
Note that the completion algorithm can be used also to check TBox consistency and concept satisifability. For the latter, we have from Lemma 4 that is unsatisfiable w.r.t. if ⊥ ∈ (). For the former, we can add the GCI ⊤ ⊑ and check whether is unsatisfiable.
/ linwith nominals would efectively give a means to identify
Admitting Nominals. Extending ℰℒ⊥
and address a particular granule in the TBox by using the concept {}. This might be useful for
some applications. The subsumption algorithm for rough ℰℒ++ in [
The reason why arbitrary classes of indiscernibility relations is problematic is that there is no way to predict the relationships between objects. For instance, we can have ∼ 1 ∼ 2 and there be no relation between and . A construction akin to our completion algorithm would need to preserve at least 2 diferent objects to keep track of this information. Yet, we still do not know whether another strategy could reduce the overall complexity to remain in polynomial time, or in a sub-exponential class.
In this paper we have extended the ℰℒ family by another rough member, that admits a (linear) hierarchy of indiscernibility relations to be used in upper and lower approximation concepts. The resulting DL / lincan facilitate reasoning w.r.t. clustering results for data that vary in granularity. For the DL ℰℒ/⊥ lin, we have devised a subsumption algorithm based on completion rules. This algorithm runs in ℰℒ⊥ polynomial time and can also be employed to test satisfiability of concepts.
/ linwould be reasoning problems that answer queries over the
The next thing to investigate for ℰℒ⊥ TBox together with an ABox. Instance checking and answering of conjunctive queries are so far only studied to a small extent for rough DLs. Usually, completion algorithms for subsumption readily extend to algorithms for instance checking, while their extension to algorithms for answering conjunctive queries is more challenging.
Rough DLs have been employed for instance unification [ 16]. A similar task is solved in entity resolution. Here, sometimes also information on non-equivalence of entities is given to avoid unification. Likewise, some applications of rough sets consider a discernibility relation in addition to the indiscernibility relation. It would be interesting to extend rough DLs by a discernibility relation that can express that two elements are not members of the same equivalence class. As such a relation introduces a form of negation, it is not immediately clear how to extend the reasoning algorithms.
Partially supported by the MUR for the Department of Excellence DISCo at the University of MilanoBicocca and under the PRIN project PINPOINT Prot. 2020FNEB27, CUP H45E21000210001; and by the European Union – Next Generation EU within the project NRPP M4C2, Investment 1.,3 DD. 341 - 15 march 2022 – FAIR – Future Artificial Intelligence Research – Spoke 4 - PE00000013 - D53C22002380006 Conference on Knowledge Engineering and Management by the Masses EKAW 2010, volume 6317 of LNCS, Springer, 2010, pp. 503–513. [15] F. Baader, S. Brandt, C. Lutz, Pushing the ℰ ℒ envelope, in: Proc. of 18th Int. Joint Conference on
Artificial Intelligence (IJCAI 2005), 2005. [16] M. C. Klein, P. Mika, S. Schlobach, Rough description logics for modeling uncertainty in instance unification, in: Proc. of 3rd ISWC Workshop on Uncertainty Reasoning for the Semantic Web, volume 327 of CEUR Workshop Notes, 2007.