=Paper=
{{Paper
|id=Vol-2214/paper2
|storemode=property
|title=Power (Set) ALC (Extended Abstract)
|pdfUrl=https://ceur-ws.org/Vol-2214/paper2.pdf
|volume=Vol-2214
|authors=Laura Giordano,Alberto Policriti
|dblpUrl=https://dblp.org/rec/conf/cilc/0001P18
}}
==Power (Set) ALC (Extended Abstract)==
https://ceur-ws.org/Vol-2214/paper2.pdf
Power (Set) ALC (Extended Abstract)
Laura Giordano1 and Alberto Policriti2
1
DISIT, Università del Piemonte Orientale, Alessandria, Italy,
laura.giordano@uniupo.it
2
Dipartimento di Scienze Matematiche, Informatiche e Fisiche, Università di Udine
Istituto di Genomica Applicata, Parco Scientifico e Tecnologico “L. Danieli”, Italy,
alberto.policriti@uniud.it
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 (possi-
bly 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, consist-
ing 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.
1 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 ∈ C 1 . 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 can-
not 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 ex-
ample 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 met-
alogical 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. De-
cidability 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 natu-
rally 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 decid-
able by defining, for any ALC Ω knowledge base K, a polynomial translation K T into
ALCOI, exploiting the correspondence studied in [3] between the membership rela-
tion in the set theory and a normal modality. From the translation in ALCOI we obtain
an E XP T IME 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
S extensionally
different—is the collection of well-founded sets HF = HF0 = n∈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 = ∆\C I
I I I
(C\D) = (C \D ) (Pow(C)) = Pow (C I ) ∩ ∆
I
I I I
(C ⊓ D) = C ∩ D (C ⊔ D)I = C I ∪ DI
(∀R.C) = {x ∈ ∆ | ∀y((x, y) ∈ RI → y ∈ C I )}
I
(∃R.C)I = {x ∈ ∆ | ∃y((x, y) ∈ RI ∧ y ∈ C I )}
Observe that A ⊆ ∆ ∈ U. The interpretation C I 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 C I 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, C I 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 C I ∈ DI ; (ii) I satisfies
(C, D) ∈ R if (C I , 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 C T 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 C T ≡ ∃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 E XP T IME upper bound for satisfiability in ALC Ω .
5 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 complete-
ness 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 Descrip-
tion Logic Handbook - Theory, Implementation, and Applications. Cambridge, 2007.
3. G. D’Agostino, A. Montanari, and A. Policriti. A set-theoretic translation method for poly-
modal 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 Theo-
retical Computer Science, Urbino, Italy, 18-20 September 2018.
6. L. Giordano and A. Policriti. Power(Set) Description Logic. In Technical Report TR-INF-
2018-02-02-UNIPMN dell’Universitá del Piemonte Orientale, Italy, February 2018.
7. B. Glimm, S. Rudolph, and J. Vö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. Svá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. Kubincová, J. Kluka, and M. Homola. Towards expressive metamodelling with instantia-
tion. 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.