We explore the relationships between Description Logics and Set Theory. The study is carried on using, on the set-theoretic side, a very rudimentary axiomatic set theory , consisting of only four axioms characterizing binary union, set difference, inclusion, and the power-set. The approach is then completed defining ALC , an extension of ALC in which concepts are naturally interpreted as sets living in -models. In ALC not only membership between concepts is allowed-even admitting circularity-but also the power-set construct is exploited to add metamodeling capabilities. We conclude providing a polynomial translation of ALC in ALCOI and proving its basic traits, among which the validity of the finite model property.
1. the possibility of having, as a special case, a concept as an instance of itself: C 2 C1; 2. the possibility of talking about all possible sub-concepts of a given concept, adding a power-set construct Pow(C).
In order to realize our plan we introduce a DL, to be dubbed ALC , whose two parents
are ALC and a rudimentary (finitely axiomatized) set theory .
1 Self membership is allowed for concept names in [
For instance, considering an example taken from [
The power-set concept, Pow(C), allows to capture in a natural way the interactions between concepts and metaconcepts. Considering again the example above, the statement “all the instances of species in the Red List are not allowed to be hunted” can be represented by the concept inclusion axiom: RedListSpecies v Pow(CannotHunt ), meaning that all the instances in the RedListSpecies (as the class Eagle) are included in CannotHunt .
Motik has shown in [
Starting from [
Here, we propose an extension of ALC with power-set concepts and membership
axioms among concepts, whose semantics is naturally defined using sets living in
models (not necessarily well-founded). We prove that ALC is decidable by defining, for
any ALC knowledge base K, a polynomial translation KT into ALCOI, exploiting
the correspondence studied in [
Let NC be a set of concept names, NR a set of role names and NI a set of individual names. The set C of ALC concepts can be defined inductively as follows: - A 2 NC , > and ? are concepts in C; - if C; D 2 C and R 2 NR, then C u D; C t D; :C; 8R:C; 9R:C are concepts in C. A knowledge base (KB) K is a pair (T ; A), where T is a TBox and A is an ABox. The TBox T is a set of concept inclusions (or subsumptions) C v D, where C; D are concepts in C. The ABox A is a set of assertions of the form C(a) and R(a; b) where C is a concept, R 2 NR, and a; b 2 NI .
An interpretation for ALC [
Given a KB K = (T ; A), an interpretation I satisfies T (resp. A) if I satisfies all inclusions in T (resp. all assertions in A); I is a model of K if I satisfies T and A. Let a query F be either an inclusion C v D (where C and D are concepts) or an assertion C(a). F is entailed by K, written K j= F , if for all models I =h ; I i of K, I satisfies F .
Given a knowledge base K, the subsumption problem is the problem of deciding whether an inclusion C v D is entailed by K. The instance checking problem is the problem of deciding whether an assertion C(a) is entailed by K. The concept satisfiability problem is the problem of deciding, for a concept C, whether C is consistent with K (i.e., whether there exists a model I of K, such that CI 6= ;).
In the following we will also consider the description logic ALCOI allowing inverse roles and nominals. For a role R 2 NR, its inverse is a role, denoted by R , which can be used in existential and universal restrictions with the following semantics: (x; y) 2 (R )I if and only if (y; x) 2 RI . For a named individual a 2 NI , the nominal fag is the concept such that: (fag)I = faI g. 2.2
The theory The first-order theory consists of the following four axioms in the language with relational symbols 2 and , and functional symbols [, n, Pow : x 2 y [ z $ x 2 y _ x 2 z; x 2 ynz $ x 2 y ^ x 62 z;
x y $ 8z(z 2 x ! z 2 y); x 2 Pow (y) $ x y:
In any -model everything is supposed to be a set. Hence, a set will have (only) sets as its elements and circular definition of sets are not forbidden—i.e., for example, there are models of in which there are sets admitting themselves as elements. Moreover, not postulating in any link between membership 2 and equality—in axiomatic terms, having no extensionality (axiom)—, there exist -models in which there are different sets with equal collection of elements.
The most natural -model—in which different sets are, in fact, always extensionally different—is the collection of well-founded sets HF = HF0 = Sn2N HFn, where: HF0 = ;;
HFn+1 = Pow (HFn): In HF0 every system of set-theoretic equations of the form: 8 x1 = fx1;1; : : : ; x1;m1 g; > >>< x2 = fx2;1; : : : ; x2;m2 g; >> ... ...
>: xn = fxn;1; : : : ; xn;mn g; where xi;j for j = 1; : : : ; mi is one among x1; : : : xi 1, finds a unique solution.
If we drop the index-ordering restriction on variables appearing in the right-hand-side
of set-theoretic equations (thereby allowing equations such as x = fxg), in order to
guarantee the existence of solutions in the model we need to work with universes larger
than HF. The most natural (and minimal) among them is a close relative of HF0 and
goes under the name of HF1=2 (see [
Finally, a further enrichment of both HF0 and HF1=2 is obtained by adding atoms, that is copies of the empty-set, to be denoted by a1; a2; : : : and collectively represented by A = fa1; a2; : : :g. The resulting universes will be denoted by HF0(A) and HF1=2(A).
A complete discussion relative to universes of sets to be used as models of goes
beyond the scope of this paper. However, it is convenient to point out that, in all cases
of interest for us here, an especially simple view of -models can be given using finite
graphs. Actually, HF0 or HF1=2 can be seen as the collection of finite graphs (either
acyclic or cyclic, respectively), where sets are represented by nodes and arcs depict the
membership relation among sets (see [
In the next section, we will regard the domain of a DL interpretation as a fragment of the universe of an -model, i.e. will be regarded as a set of sets of the theory rather than as a set of individuals, as customary in description logics. 3
We start from the observation that in ALC concepts are interpreted as sets (namely, sets of domain elements) and we generalize ALC by allowing concepts to be interpreted as sets of the set theory . In addition, we extend the language of ALC by introducing the power-set as a new concept constructor, and allowing membership relations among concepts in the knowledge base. We call ALC the resulting extension of ALC.
As before, let NI , NC , and NR be the set of individual names, concept names, and role names in the language, respectively. In building complex concepts, in addition to the constructs of ALC, we also consider the difference n and the power-set Pow constructs. The set of ALC concepts are defined inductively as follows: – A 2 NC , > and ? are ALC concepts; – if C; D are ALC concepts and R 2 NR, then the following are ALC concepts:
C u D; C t D; :C; CnD; Pow(C); 8R:C; 9R:C While the concept CnD can be easily defined as C u :D in ALC, this is not the case for the concept Pow(C). Informally, the instances of concept Pow(C) are all the subsets of the instances of concept C visible in the domain (see below).
Besides ABox assertions of the form C(a) with a 2 NI , we allow in the ABox concept membership axioms and role membership axioms, respectively, of the form: C 2 D and (C; D) 2 R, where C and D are ALC concepts and R is a role name.
Considering again the example from the Introduction, the additional expressivity of
the language, in which general concepts (and not only concept names) can be instances of
other concepts, allows for instance to represent the fact that polar bears are in the red list
of endangered species, by the axiom Polar u Bear 2 RedListSpecies . We can further
represent the fact the polar bears are more endangered than eagles by adding a role
moreEndangered and the role membership axiom (Polar u Bear ; Eagle) 2
moreEndangered . Observe that, as shown in [
We define a semantics for ALC by extending the ALC semantics in Section 2.1 to capture the meaning of concepts (including concept Pow(C)) as elements (sets) of the domain , chosen as a transitive set (i.e. a set x satisfying (8y 2 x)(y x)) in a model of . Roles are interpreted as binary relations over the domain . Individual names are interpreted as elements of a set of atoms A from which the sets in are built. Definition 2. An interpretation for ALC is a pair I = h ; I i over a set of atoms A where: – the non-empty domain is a transitive set chosen in a model M of over the atoms in A (we let U be the universe of the model M);2 – the extension function I maps each concept name A 2 NC to an element AI 2 ; each role name R 2 NR to a binary relation RI ; and each individual name a 2 NI to an element aI 2 A .
The function I is extended to complex concepts of ALC , as in Section 2.1 for ALC, but for the two additional cases: (Pow(C))I = Pow (CI ) \ and (CnD)I = (CI nDI ). Observe that A 2 U . As is not guaranteed to be closed under union, intersection, etc., the interpretation CI of a concept C is a set in U but not necessarily an element 2 In the following, for readability, we will denote by 2, Pow , [, n (rather than Pow M, [M, nM) the interpretation in a model M of the predicate and function symbols 2, Pow , [, n. of . However, given the interpretation of the power-set concept as the portion of the (set-theoretic) power-set visible in , it easy to see by induction that, for each C, the extension of CI is a subset of .
Given an interpretation I, the satisfiability of inclusions and assertions is defined as in ALC interpretations (Definition 1). Satisfiability of (concept and role) membership axioms in an interpretation I is defined as follows: I satisfies C 2 D if CI 2 DI ; I satisfies (C; D) 2 R if (CI ; DI ) 2 RI . With this addition, the notions of satisfiability of a KB and of entailment in ALC (denoted j=ALC ) can be defined as in Section 2.1.
The problem of instance checking in ALC includes both the problem of verifying whether an assertion C(a) is a logical consequence of the KB and the problem of verifying whether a membership C 2 D is a logical consequence of the KB (i.e., whether C is an instance of D).
In the next section, we define a polynomial encoding of the language ALC into the description logic ALCOI. 4
into ALCOI
To provide a proof method for ALC , we define a translation of ALC into the
description logic ALCOI, including inverse roles and nominals. In [
The translation of an ALC knowledge base K = (T ; A) into ALCOI can be defined as follows. First, we associate each concept C of ALC to a concept CT of ALCOI by replacing all occurrences of the power-set constructor Pow with a concept involving the universal restriction 8e (see below). More formally, we (inductively) define the translation CT of C by simply recursively replacing every subconcept Pow(D) appearing in C by 8e:DT , while the translation T commutes with concept constructors in all other cases.
Semantically this will result in interpreting any (sub)concept (Pow(D))I by (8e:D)I = fx 2
j 8y((x; y) 2 eI ! y 2 DI )g; which, recalling that (x; y) 2 eI stands for y 2 x, will characterize the collection of subsets of DI visible in (i.e. subsets of DI which are also elments of ): (8e:D)I = fx 2 j 8y(y 2 x ! y 2 DI )g, that is, (8e:D)I = fx 2 j x DI )g = Pow(DI ) \ = (Pow(D))I , as expected. 4.1
Translating TBox, ABox, and queries We define a new TBox, T T , by introducing, for each inclusion C v D in T , the inclusion CT v DT in T T . Additionally, for each (complex) concept C occurring in the knowledge base K (or in the query) on the l.h.s. of a membership axiom C 2 D (1) or (C; D) 2 R, we extend NI with a new individual name3 eC and we add the concept equivalence:
CT
9e :feC g: in T T . From now on, new individual names such as eC will be called concept individual names. This equivalence is intended to capture the property that, in all the models I = h ; I i of KT , eIC is in relation eI with all and only the instances of concept CT , i.e., for all y 2 , (eIC ; y) 2 eI if and only if y 2 (CT )I .
As in the case of the power-set constructor, this fact can be verified by analyzing the semantics of 9e :feC g: (9e :feC g)I = fx 2
j 9y((x; y) 2 (e )I ^ y 2 (feC g)I g; which, recalling that e stands for 3 and interpreting the nominal, will stand for (9e :feC g)I = fx 2
I j 9y(x 2 y ^ y 2 feC gg = fx 2 j x 2 eIC g; which, by the concept equivalence CT have the same extension.
9e :feC g, is as to say that eIC and (CT )I Remark 1. It is important to notice that every concept individual name of the sort eC introduced above—that is, every individual name whose purpose is that of providing a name to the extension of CI —, in general turns out to be in relation e with other elements of the domain of I (unless C is an inconsistent concept and its extension is empty). This is in contrast with the assumption relative to other “standard” individual names a 2 NI , for which we will require (:9e:>)(a) (see below).
We define AT as the set of assertions containing: – for each concept membership axiom C 2 D in A, the assertion DT (eC ), – for each role membership axiom (C; D) 2 R in A, the assertion R(eC ; eD), – for each assertion D(a) in A, the assertion DT (a), – for each assertion R(a; b) in A, the assertion R(a; b) and, finally, – for each (standard) individual name a 2 NI , the assertion (:9e:>)(a). As noticed above, the last requirement forces all named individuals (in the language of the initial knowledge base K) to be interpreted as domain elements which are not in relation e with any other element.
Let KT = (T T ; AT ) be the knowledge base obtained by translating K into ALCOI. Example 1. Let K = (T ; A) be the knowledge base considered above: T = fRedListSpecies v Pow(CannotHunt )g and
A = fEagle(harry ); Eagle 2 RedListSpecies ; Polar u Bear 2 RedListSpecies g. By the translation above, we obtain:
T T = fRedListSpecies v 8e:CannotHunt ;
Eagle 9e :feEagle g; Polar u Bear 9e :fePolaruBear g g AT = fEagle(harry ); RedListSpecies (eEagle ); RedListSpecies (ePolaruBear ); (:9e:>)(harry ) g 3 The symbol eC should remind the e-xtension of C. KT entails CannotHunt (harry ) in ALCOI. In fact, from RedListSpecies (eEagle ) and RedListSpecies v 8e:CannotHunt , it follows that, in all models of KT , eIEagle 2 (8e:CannotHunt )I . Furthermore, from Eagle 9e :feEagle g and the assertion Eagle(harry ), it follows that (eEIagle ; harry I ) 2 eI holds. Hence, harry I 2 Cannot Hunt I . As this holds in all models of KT , CannotHunt (harry ) is a logical consequence of KT . It is easy to see that Eagle v CannotHunt follows from KT as well.
Let F be a query of the form C v D, C(a) or C 2 D We assume that all the individual names, concept names and role names occurring in F also occur in K and we define a translation F T of the query F as follows: – if F is a subsumption C v D, then F T is the subsumption CT v DT ; – if F is an assertion C(a), then F T is the assertion CT (a); – if F is a membership axiom C 2 D (respectively, (C ; D ) 2 R), then F T is the assertion DT (eC ) (respectively, R(eC ; eD )).
In the following we state the soundness and completeness of the translation of an ALC knowledge base into ALCOI.
base K = (T ; A) into ALCOI is sound, that is, for any query F : knowledge KT = j ALCOI F T ) K j=ALC
F:
For the sake of brevity a proof of the above proposition, which is given along standard lines, is not given here.
Before proving the completeness of the translation of ALC that, if the translation KT of a knowledge base K in ALC then it also has a finite model.
into ALCOI, we show has a model in ALCOI, Proposition 2. Let K be a knowledge base in ALC and let KT be its translation in ALCOI. If KT has a model in ALCOI, then it has a finite model.
Proof. We prove this result by providing an alternative (but equivalent) translation KT (:) of K in the description logic ALC(:), using a single negated role :e.
ALC(:) extends ALC with role complement operator, where, for any role R, the
role :R is the negation of role R, where (x; y) 2 (:R)I if and only if (x; y) 62 RI . In
the translation, we exploit :e to capture non-membership, where (x; y) 2 (:e)I if and
only if (x; y) 62 eI (i.e., in set terms, y 62 x). Decidability of concept satisfiability in
ALC(:) has been proved by Lutz and Sattler in [
The translation KT (:) can be defined modifying KT by replacing the concept equivalence CT 9e :feC g with the assertions: (8e:CT )(eC ) and (8(:e):(:CT ))(eC ).
One can show that any model I = ( ; I ) of KT (:) is a model of KT in ALCOI, and vice-versa (considering the usual interpretation of negated roles, inverse roles and nominals). In fact, the semantic meaning of the assertion (8e:CT )(eC ) is the following: for all x 2
, (eIC ; x) 2 eI ) x 2 (CT )I , which is equivalent to the meaning of 9e :feC g v CT .
The semantic meaning of the assertion (8(:e):(:CT ))(eC ) is: for all x 2 , (eIC ; x) 62 eI ) x 62 (CT )I , i.e., for all x 2 , x 2 (CT )I ) (eIC ; x) 2 eI , which is the semantic meaning of CT v 9e :feC g.
We conclude the proof by observing that, if KT has a model, it is a model of KT (:). Then, by the finite model property, KT (:) must have a finite model which is, in turn, a finite model of KT . 2
To conclude our analysis we now prove the completeness of our translation.
edge base K = (T ; A) into ALCOI is complete, that is, for any query F : knowlK j=ALC
F ) KT j=ALCOI F T : Proof (sketch). The proof is by contraposition. Assume that KT = 6j ALCOI F T . Then there is a model I = h ; I i of KT in ALCOI such that I falsifies F .
We show that we can build a model J = h ; J i of K in ALC , where the domain is a transitive set in the universe HF1=2(A) consisting of all the hereditarily finite rational hypersets built from atoms in A = fa0; a1; : : :g.
We define starting from the graph4 G = h ; eI i, whose nodes are the elements of and whose arcs are the pairs (x; y) 2 eI . Notice that, by Proposition 2, the graph G can be assumed to be finite. Intuitively, an arc from x to y in G stands for the fact that y 2 x.
At this point, let 0 = fd1; : : : ; dmg be the elements of which, in the model I = h ; I i, are not in relation eI with any other element in and are non equal to the interpretation of any concept individual name eC (that is, dj 2 0 iff there is no y such that (dj ; y) 2 eI and there is no concept C such that dj = eIC ). For any given d 2 we define the following hyperset M (d):
M (d) = ak
M (d0) j (d; d0) 2 eI if d = dk 2 otherwise.
0; (2) Observe that, for the concepts C occurring on the l.h.s. of membership axioms, as axiom CT 9e :feC g is satisfied in the model I of KT , it holds that d0 2 (CT )I iff (eIC ; d0) 2 eI . Therefore, for d = eIC , M (d) = M (eIC ) = M (d0) j (eIC ; d0) 2 eI = M (d0) j d0 2 (CT )I .
The above definition uniquely determines hypersets in HF1=2(A). This follows
from the fact that all finite systems of (finite) set-theoretic equations have a solution in
HF1=2(A). As a matter of fact, whenever the graph G is acyclic, the definition of M (d)
identifies a standard (recursively given) hereditarily finite set5.
4 Strictly speaking the graph G introduced here is not really necessary: it is just mentioned to
single out the membership relation 2 from eI more clearly.
5 More generally, when eI is a well-founded relation, M ( ) is a set-theoretic “rendering” of eI :
the so-called Mostowski collapse of eI (see [
Our task now is to complete the definition of J = h ; J i in such a way to prove that J is a model of K in ALC falsifying F . The definition is completed as follows: – = fM (d) j d 2 g; – for all B 2 NC , BJ = fM (d) j d 2 BI g; – for all roles R 2 NR such that R 6= e, RJ = f(M (d); M (d0)) j (d; d0) 2 RI g; – for all standard name individuals a 2 NI such that aI = dk, let aJ = M (dk) = ak 2 A.
To complete the proof it can be shown that, for all d 2 , M (d) 2 CJ if and only if d 2 (CT )I , which is used to show that J is a model of K that falsifies F. 2
As the translation of ALC into ALCOI is polynomial (actually, linear) in the size of the knowledge base (and of the query) the following complexity result follows. Proposition 4. Concept satisfiability in ALC is an EXPTIME-complete problem.
The hardness comes from the EXPTIME-hardness of ALC concept satisfiability w.r.t. a
set of inclusions [
In this paper we have shown that the similarities between description logics and set theory can be exploited to introduce in DLs the new power-set construct and to allow for (possibly circular) membership relationships among arbitrary concepts. We have defined the description logic ALC , combining ALC with the set theory , and defined its semantics whose interpretation domains are fragments of the domains of -models. ALC allows membership axioms among concepts as well as the power-set construct which, up to our knowledge, has not been considered for description logics before. We have shown that an ALC knowledge base can be polynomially translated into an ALCOI knowledge base. Soundness and completeness of the translation provide, besides decidability, an EXPTIME upper bound for satisfiability in ALC .
The power-set construct allows to capture in a very natural way the interactions
between concepts and metaconcepts, adding to the language of ALC the expressivity
of metamodelling. The issue of metamodelling has been analysed by Motik in [
As in [
In Hi (SHIQ) [
Kubincova et al. in [
Pan and Horrocks in [
In [
A set-theoretic approach in DLs has been adopted by Cantone et al. in [
We expect that the approach of extending ALC with can be adopted as well for more expressive DLs, which do not enjoy the finite model property. However, when the finite model property does not hold, there may be models of the translated knowledge base KT containing domain elements being in the relation e with infinitely many elements, and corresponding to infinite sets. The completeness proof of Proposition 3 does not apply to this case and we leave the study of this case for future investigation.
Other possible directions for future investigation concern: the treatment of roles as individuals, which has not been considered as an option in ALC ; restricting the semantics to well-founded sets to avoid circular definitions of sets; translating ALC into the set theory , which may open to the possibility of exploiting proof methods developed for set theories in reasoning with DLs, as an alternative to translating to DLs.
Acknowledgement: This research is partially supported by INDAM-GNCS Project 2018 “Metodi di prova orientati al ragionamento automatico per logiche non-classiche”.