Power (Set) ALC (Extended Abstract)

Abstract

The similarities between Description Logics (DLs) and Set Theory can be exploited to introduce in DLs a power-set concept and to allow for (possibly circular) membership relationships among arbitrary concepts. In this abstract, we describe the main ideas underlying the definition of ALCΩ, a description logic combining ALC with Ω, a very rudimentary axiomatic set theory, consisting of only four axioms characterizing binary union, set difference, inclusion, and the power-set. In ALCΩ , concepts are naturally interpreted as sets living in Ω-models. The power-set concept and the membership axioms among concepts give useful metamodeling capabilities to the language.

Introduction

The relationships between Description Logics (DLs) and Set Theory are strong. If not for other reasons, just considering the fact that concepts in DLs are interpreted as sets of domain elements and that the basic concept constructs in DLs, namely intersection, union and complement, are the very basic notions of any (axiomatic) set theory.

We aim at enhancing the relations between DLs and the Set Theory, by considering the very simple axiomatic set theory Ω—consisting of only four axioms characterizing binary union, set difference, inclusion, and the power-set—and extending DLs with new constructor for concepts, the power-set and the set-difference constructs, as specified in Ω. In addition, we want to use concept membership axioms of the form C ∈ D, stating that the concept C is an instance of concept D, and role membership axioms of the form (C, D) ∈ R, stating that concept C is in relation R with concept D. This extension is very natural considering that concepts can be interpreted as sets living in Ω-models, where each set can only have other sets as elements.

Furthermore, we do not require sets to be well-founded, as in [ 15, 13 ], and therefore we open up to the possibility of having a concept as an instance of itself: C ∈ C1. For instance, considering an example taken from [ 16, 12 ], using membership axioms, we can represent the fact that eagles are in the red list of endangered species, by the axiom Eagle ∈ RedListSpecies and that Harry is an eagle, by the assertion Eagle(harry ). We could further consider a concept notM odif iableList, consisting of those list that cannot be modified (if not by, say, a specifically enforced law) and, for example, it would be 1 Self membership is already allowed for concept names in [ 12 ], by assertions of the form a(a). reasonable to ask RedListSpecies ∈ notModifiableList . However, more interestingly, we would also clearly want notModifiableList ∈ notModifiableList .

The power-set concept, Pow(C), allows us to talk about all possible sub-concepts of a given concept C visible in the domain, and it allows us also 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 ⊑ Pow(CannotHunt ), meaning that all instances of the classes in the RedListSpecies (as Eagle) are included in CannotHunt .

Motik has shown in [ 12 ] that the semantics of metamodeling adopted in OWL-Full leads to undecidability already for ALC-Full, due to the free mixing of logical and metalogical symbols. In [ 12 ], limiting this free mixing but allowing names to be interpreted as concepts and to occur as instances of other concepts, two alternative semantics (the Contextual π-semantics and the Hilog ν-semantics) are proposed for metamodeling. Decidability of SHOIQ extended with metamodeling is proved under either semantics. As shown in [ 12 ], the meaning of the sentence above could be captured by combining the ν-semantics with SWRL [ 10 ], but not by the ν-semantics alone.

Starting from [ 12 ], many other approaches to metamodeling have been proposed in the literature. Most of them [ 4, 9, 11, 8 ] are based on a Hilog semantics, while [ 15, 13 ] define extensions of OWL DL and of SHIQ (respectively), based on semantics interpreting concepts as well-founded sets. 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 (which are not necessarily well-founded).

In the following we shortly describe an extension of ALC, ALCΩ, including the power-set concept and concept membership axioms, which we have proved to be decidable by defining, for any ALCΩ knowledge base K, a polynomial translation KT into ALCOI, exploiting the correspondence studied in [ 3 ] between the membership relation in the set theory and a normal modality. From the translation in ALCOI we obtain an EXPTIME upper bound on the complexity of satisfiability in ALCΩ . Interestingly enough, our translation has strong relations with the first-order reductions used in [ 7, 9, 11 ]. An extended version of this work will appear in [ 5 ]. 2

The theory Ω The first-order theory Ω consists of the following four axioms in the language with relational symbols ∈ and ⊆, and functional symbols ∪, \, Pow : x ∈ y ∪ z ↔ x ∈ y ∨ x ∈ z; x ∈ y\z ↔ x ∈ y ∧ x 6∈ z;

x ⊆ y ↔ ∀z(z ∈ x → z ∈ y); x ∈ Pow (y) ↔ x ⊆ y.

In an Ω-model everything is supposed to be a set. Hence, a set will have (only) sets as its elements and circular definition of sets are allowed (such as a set admitting itself as one of its elements). Moreover, not postulating in Ω any link between membership ∈ and equality—in axiomatic terms, having no extensionality (axiom)—Ω-models in which there are different sets with equal collection of elements, are admissible.

The most natural Ω-model—in which different sets are, in fact, always extensionally different—is the collection of well-founded sets HF = HF0 = Sn∈N HFn, where: HF0 = ∅ and HFn+1 = Pow (HFn). A close relative of HF0, in which sets are not required to be well-founded, goes under the name of HF1/2 (see [ 1, 14 ]). HF0 or HF1/2 can be seen as the collection of finite (either acyclic or cyclic) graphs where sets are represented by nodes and arcs depict the membership relation among sets (see [ 14 ]).

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 = {a1, a2, . . .}. The resulting universes will be denoted by HF0(A) and HF1/2(A).

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

The description logic ALCΩ

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 [ 2 ], we also consider the difference \ and the power-set Pow constructs. The set of ALCΩ concepts are defined inductively as follows: – A ∈ NC , ⊤ and ⊥ are ALCΩ concepts; – if C, D are ALCΩ concepts and R ∈ NR, then the following are ALCΩ concepts:

C ⊓ D, C ⊔ D, ¬C, C\D, Pow(C), ∀R.C, ∃R.C While the concept C\D can be easily defined as C ⊓ ¬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.

Besides ABox assertions of the form C(a) with a ∈ NI , we allow in the ABox concept membership axioms and role membership axioms, respectively, of the form: C ∈ D and (C, D) ∈ R, where C and D are ALCΩ concepts and R is a role name.

The additional expressivity of the language, allows for instance to represent the fact that polar bears are in the red list of endangered species, by axiom Polar ⊓ Bear ∈ RedListSpecies , and that the polar bears are more endangered than eagles by adding a role moreEndangered and axiom (Polar ⊓ Bear , Eagle) ∈ moreEndangered .

The semantics for ALCΩ is defined interpreting concepts as elements (sets) in the universe U of an Ω-model, In particular, a distinguished transitive set Δ (i.e. a set x satisfying (∀y ∈ x)(∀z ∈ y)(z ∈ x)) in U is considered.

Definition 1. 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 2 In the following, for readability, we will denote by ∈, Pow , ∪, \ (rather than Pow M, ∪M, \M) the interpretation in a model M of the predicate and function symbols ∈, Pow , ∪, \, respectively. – the extension function ·I maps each concept name A ∈ NC to an element AI ∈ Δ; each role name R ∈ NR to a binary relation RI ⊆ Δ × Δ; and each individual name a ∈ NI to an element aI ∈ A ⊆ Δ. The function ·I is extended to complex concepts of ALCΩ as follows: ⊤I = Δ ⊥I = ∅ (¬C)I = Δ\CI (C\D)I = (CI \DI ) (Pow(C))I = Pow (CI ) ∩ Δ (C ⊓ D)I = CI ∩ DI (C ⊔ D)I = CI ∪ DI (∀R.C)I = {x ∈ Δ | ∀y((x, y) ∈ RI → y ∈ CI )} (∃R.C)I = {x ∈ Δ | ∃y((x, y) ∈ RI ∧ y ∈ CI )} Observe that A ⊆ Δ ∈ U . The interpretation CI of a concept C can be regarded both as an element in U (the intention of the set) and as a subset of U (the extension of the set). The semantics of standard DL concept constructs is defined as usual but, as Δ is not guaranteed to be closed under union, intersection, etc., the interpretation CI of a concept C is in U but not necessarily in Δ. However, given the interpretation of the power-set concept as the portion of the (set-theoretic) power-set visible in Δ, it is easy to see by induction that, for each C, CI is a subset of Δ.

Given an interpretation I, the usual notion of satisfiability in ALC is extended to membership axioms as follows: (i) I satisfies C ∈ D if CI ∈ DI ; (ii) I satisfies (C, D) ∈ R if (CI , DI ) ∈ RI . Given a knowledge base K = (T , A), an interpretation I satisfies T (resp. A) if I satisfies all inclusions in T (resp. all axioms in A); I is a model of K if I satisfies T and A.

Let a query F be either an inclusion C ⊑ D (where C and D are concepts), an assertion, or a membership axiom. F is entailed by K, written K |= F , if for all models I =hΔ, ·I i of K, I satisfies F . The problem of instance checking in ALCΩ includes the problem of verifying whether a membership C ∈ D is a logical consequence of the KB (i.e., whether C is an instance of D). 4

Translation of ALCΩ into ALCOI

A translation of the logic ALCΩ into the description logic ALCOI, including inverse roles and nominals, can be defined based on the correspondence between ∈ and the accessibility relation of a modality explored in [ 3 ]. There, the membership relation ∈ is used to represent a normal modality R. Here, vice-versa, a new (reserved) role e in NR is introduced to represent the inverse of the membership relation, restricted to the sets in Δ: in any interpretation I, (x, y) ∈ eI will stand for y ∈ x. The idea underlying the translation is that each element u of the domain Δ in an ALCOI interpretation I = hΔ, ·I i can be regarded as the set of all the elements v such that (u, v) ∈ eI .

The translation of a KB K = (T , A) of ALCΩ into ALCOI can be defined by replacing each concept C in K with a concept CT of ALCOI, where all occurrences of the power-set concept Pow(D) are recursively replaced by ∀e.DT . A new individual name eC is also introduced for each concept name C occurring on the left hand side of a membership axiom. By axiom CT ≡ ∃e−.{eC }, the role e relates eC with all the instances of concept C. Each membership axiom C ∈ D can then be translated to an assertion DT (eC ). Soundness and completeness of the translation in ALCOI (see [ 5, 6 ]) provide, besides decidability, an EXPTIME upper bound for satisfiability in ALCΩ .

Conclusions

We expect that the approach of extending ALC with Ω can also be adopted for more expressive DLs, which do not enjoy the finite model property. The proof of completeness of the translation in [ 5 ] does not apply to this case, which will be subject of future investigation. Other directions for future investigation concern: the treatment of roles as individuals; 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 for reasoning in extended DLs.

Acknowledgement: This research is partially supported by INDAM-GNCS Project 2018 “Metodi di prova orientati al ragionamento automatico per logiche non-classiche”.

References

1. P. Aczel. Non-Well-Founded Sets , volume 14 . CSLI Lecture Notes , Stanford, CA, 1988 .

2. F. Baader , D. Calvanese , D.L. McGuinness , D. Nardi , and P.F. Patel-Schneider. The Description Logic Handbook - Theory , Implementation, and Applications . Cambridge, 2007 .

3. G. D'Agostino , A. Montanari , and A. Policriti . A set-theoretic translation method for polymodal logics . J. Autom. Reasoning , 15 ( 3 ): 317 - 337 , 1995 .

4. G. De Giacomo , M. Lenzerini , and R. Rosati . Higher-order description logics for domain metamodeling . In Proc. AAAI 2011 , San Francisco, California, USA, August 7- 11 , 2011 .

5. L. Giordano and A. Policriti. Power(Set) ALC. In ICTCS , 19th Italian Conference on Theoretical Computer Science, Urbino, Italy, 18 - 20 September 2018 .

6. L. Giordano and A. Policriti. Power(Set) Description Logic . In Technical Report TR-INF2018-02-02-UNIPMN dell'Universit a´ del Piemonte Orientale , Italy, February 2018 .

7. B. Glimm , S. Rudolph , and J. Vo ¨lker. Integrated metamodeling and diagnosis in OWL 2 . In ISWC 2010, Shanghai, China, November 7- 11 , 2010 , pages 257 - 272 , 2010 .

8. Z. Gu . Meta-modeling extension of horn-sroiq and query answering . In Proceedings of the 29th Int. Workshop on Description Logics , Cape Town, South Africa, April 22-25 , 2016 .

9. M. Homola , J. Kluka , V. Sva´tek, and M. Vacura . Typed higher-order variant of SROIQ - why not? In Proc. 27th Int. Workshop on Description Logics , Vienna, Austria, July 17-20 , pages 567 - 578 , 2014 .

10. I. Horrocks and P.F. Patel-Schneider . A Proposal for an OWL Rule Language . In Proc.WWW 2004 . ACM, 2004 .

11. P. Kubincova´, J. Kluka , and M. Homola . Towards expressive metamodelling with instantiation . In Proc. of the 28th Int. Workshop on Description Logics , Athens, June 7-10, 2015 .

12. B. Motik . On the properties of metamodeling in OWL . In Proc. ISWC 2005 , 4th International Semantic Web Conference, Galway, Ireland, November 6- 10 , 2005 , pages 548 - 562 , 2005 .

13. R. Motz , E. Rohrer, and P. Severi . The description logic SHIQ with a flexible meta-modelling hierarchy . J. Web Sem ., 35 : 214 - 234 , 2015 .

14. E.G. Omodeo , A. Policriti , and A.I. Tomescu . On Sets and Graphs. Perspectives on Logic and Combinatorics . Springer, DOI 10 .1007/978-3- 319 -54981- 1 , 2017 .

15. J.Z. Pan , I. Horrocks , and G Schreiber . OWL FA: A metamodeling extension of OWL DL . In Proc.OWLED 2005 Workshop , Galway, Ireland, November 11-12 , 2005 .

16. C. Welty and D. Ferrucci . What's in an instance? Technical Report 94-18 , Max- Plank-Institut, 1994 , RPI computer Science, 1994 .