=Paper=
{{Paper
|id=Vol-2954/paper-22
|storemode=property
|title=Category-theoretical Semantics of the Description Logic ALC
|pdfUrl=https://ceur-ws.org/Vol-2954/paper-22.pdf
|volume=Vol-2954
|authors=Chan Le Duc
|dblpUrl=https://dblp.org/rec/conf/dlog/Duc21
}}
==Category-theoretical Semantics of the Description Logic ALC==
https://ceur-ws.org/Vol-2954/paper-22.pdf
Category-theoretical Semantics of the Description Logic
ALC
Chan Le Duc
Université Sorbonne Paris Nord, Laboratory in Medical Informatics and Knowledge
Engineering in e-Health (LIMICS)
chan.leduc@univ-paris13.fr
Abstract. Category theory can be used to state formulas in First-Order Logic
without using set membership. Several notable results in logic such as proof of
the continuum hypothesis can be elegantly rewritten in category theory. We pro-
pose in this paper a reformulation of the usual set-theoretical semantics of the de-
scription logic ALC by using categorical language. In this setting, ALC concepts
are represented as objects, concept subsumptions as arrows, and memberships as
logical quantifiers over objects and arrows of categories. Such a category-theore-
tical semantics provides a more modular representation of the semantics of ALC
and a new way to design algorithms for reasoning.1
1 Introduction
Languages based on Description Logics (DLs) [1] such as OWL [2], OWL2 [3], are
widely used to represent ontologies in semantics-based applications. ALC is the small-
est DL involving roles which is closed under negation. It is a suitable logic for a first
attempt to replace the usual set-theoretical semantics by another one. A pioneer work by
Lawvere [4] provided an appropriate axiomatization of the category of sets by replac-
ing set membership with the composition of functions. However, it was not indicated
whether the categorial axioms are “semantically” equivalent to the axioms based on set
membership. As pointed out by Goldblatt [5], this may lead to a very different semantics
for negation.
There have been very few works on connections between category theory and DLs.
Spivak et al. [6] used category theory to define a high-level and graphical language
comparable with OWL for knowledge representation rather than a foundational for-
malism for reasoning. In this paper, we propose a rewriting of the usual set-theoretical
semantics of ALC by using objects and arrows, which are two fundamental elements of
category theory, to represent concepts and subsumptions respectively.
Example 1. We would like to model states of a meeting such as arrived, filled-room,
starting, started, finished; and a chronological order between these states as depicted
in Figure 1. If we use concepts and subsumptions in ALC to represent the states and
order under set-theoretical semantics, then each such a concept should represent a set
1
Copyright c 2021 for this paper by its authors. Use permitted under Creative Commons Li-
cense Attribution 4.0 International (CC BY 4.0)
filled-room starting started
arrived finished
Fig. 1: Objects and arrows for a meeting
of time-points. This might not be compatible with the semantics of subsumptions with
set membership since, for instance a time-point in filled-room cannot belong to finished
(at least this is not our modelling intention). If we use roles to model this chronological
order, then transitive roles which are not allowed in ALC, should be needed to infer the
dashed relationship. However, objects and arrows under category-theoretical semantics
can be straightforwardly used to represent such states and chronological order without
referring to set membership. Moreover, transitive relationships such as the dashed one
can be inferred under category-theoretical semantics.
The paper is organized as follows. We begin by translating semantic constraints re-
lated to each ALC constructor into arrows between objects. Then, we check whether
the obtained arrows allow to restore usual properties. If it is not the case, we add new
arrows and objects for capturing the missing properties without going beyond the set-
theoretical semantics. For instance, it does not suffice to define category-theoretical
semantics of negation ¬C by stating C u ¬C −→ ⊥ and > −→ C t ¬C because it is
not possible to obtain arrows such as C ← −−
−−
→ ¬¬C from this definition (cf. Example 3).
After providing category-theoretical semantics of each constructor, unsatisfiability of
an ALC concept C with respect to an ontology is reducible to the existence of a cat-
egory consisting of an arrow C −→ ⊥. As a main result of the paper, we show that
an ALC concept is category-theoretically unsatisfiable iff it is set-theoretically unsat-
isfiable. This result allows us not only to employ objects and arrows to design reason-
ing procedures in the new setting, but also to identify interesting sublogics by remov-
ing/weakening some arrows from categorial definitions. Because of lack of place, we
refer the readers to [7] for complete proofs.
2 Syntax and set-theoretical semantics of ALC
We present syntax and semantics of the Description Logic ALC [1] with TBoxes and
some basic inference problems.
Definition 1 (Syntax and set-theoretical semantics). Let R and C be non-empty sets
of role names and concept names respectively. The set of ALC-concepts is inductively
defined as the smallest set containing all concept names in C with >, ⊥ and complex
concepts that are inductively defined as follows: C uD, C tD, ¬C, ∃R.C, ∀R.C where
C and D are ALC-concepts, and R is a role name in R. An axiom C v D is called
a general concept inclusion (GCI) where C, D are (possibly complex) ALC-concepts.
An ALC ontology O is a finite set of GCIs.
An interpretation I = h∆I , ·I i consists of a non-empty set ∆I (domain), and a
function ·I (interpretation function) which associates a subset of ∆I to each concept
name, an element in ∆I to each individual, and a subset of ∆I × ∆I to each role name
such that
>I = ∆I , ⊥I = ∅, (¬C)I = ∆I \ C I
(C u D) = C I ∩ DI , (C t D)I = C I ∪ DI
I
(∃R.C)I = {x ∈ ∆I | ∃y ∈ ∆I ,hx, yi ∈ RI ∧y ∈ C I }
(∀R.C)I = {x ∈ ∆I | ∀y ∈ ∆I , hx, yi ∈ RI =⇒ y ∈ C I }
An interpretation I satisfies a GCI C v D if C I ⊆ DI . I is a model of O, written
I |= O, if I satisfies each GCI in O. In this case, we say that O is set-theoretically
consistent, and set-theoretically inconsistent otherwise. A concept C is set-theoretically
satisfiable with respect to O if there is a model I of O such that C I 6= ∅, and set-
theoretically unsatisfiable otherwise. We say that a GCI C v D is set-theoretically
entailed by O, written O |= C v D, if C I ⊆ DI for all models I of O. The pair
hC, Ri is called the signature of O.
3 Category-theoretical semantics of ALC
We can observe that the set-theoretical semantics of ALC is based on set membership
relationships while ontology inferences such as consistency, concept subsumption in-
volve set inclusions. This explains why inference algorithms developed in this setting
build often a set of individuals connected in some way for representing a model.
In this section, we use some basic notions in category theory to characterize the
semantics of ALC. Instead of set membership, we use in this categorical language ob-
jects and arrows to define semantics of a given object. Although the present paper is
self-contained, we refer the readers to textbooks [5,8] on category theory for further
information.
Definition 2 (Syntax categories). Let R and C be non-empty sets of role names and
concept names respectively. We define a concept syntax category Cc and a role syntax
category Cr from the signature hC, Ri as follows:
1. Each object of Cc is an ALC-concept built from hC, Ri. In particular, ⊥ and >
are respectively initial and terminal objects, i.e. there are arrows C −→ > and
⊥ −→ C for each object C of Cc . Furthermore, there is an identity arrow C −→ C
for each object C of Cc .
2. Each object of Cr is a role name R in R or R(∃R.C) defined for each object ∃R.C in
Cc . There are initial and terminal objects R⊥ and R> in Cr with arrows R −→ R>
and R⊥ −→ R for all object R of Cr . Furthermore, there is an identity arrow
R −→ R for each object R of Cr .
3. If there are arrows E −→ F and F −→ G in Cc or Cr , then there is an arrow
E −→ G.
4. There are two functors dom and cod from Cr to Cc , i.e. they associate two objects
dom(R) and cod(R) of Cc to each object R of Cr such that identity arrows and
arrow compositions are preserved from Cr to Cc as follows:
(a) if there is an arrow R −→ R in Cr then there are arrows dom(R) −→ dom(R)
and cod(R) −→ cod(R) in Cc ,
(b) if there are arrows R −→ R0 −→ R00 in Cr then there are arrows dom(R) −→
dom(R00 ) and cod(R) −→ cod(R00 )
For each arrow E −→ F in Cc or Cr , E and F are respectively called domain and
codomain of the arrow. We use also Ob(C ) and Hom(C ) to denote the collections of
objects and arrows of a category C .
In this paper, an object of Cc and Cr is called concept and role object respectively.
We transfer the vocabulary used in Description Logics to categories as follows. A con-
cept object C t D, C u D or ¬C is respevtively called disjunction, conjunction and
negation object. For an existential restriction object ∃R.C or universal restriction ob-
ject ∀R.C, C is called the filler of ∃R.C and ∀R.C.
In the sequel, we introduce category-theoretical semantics of disjunction, conjunc-
tion, negation, existential and universal restriction objects by adding arrows to Cc . Some
of them require more explicit properties than those needed for the set-theoretical se-
mantics. This is due to the fact that set membership is translated into arrows in a syntax
category.
Definition 3 (Category-theoretical semantics of disjunction). Let C, D, C t D be
concept objects of Cc . Category-theoretical semantics of C t D is defined by using
arrows in Cc as follows. There are arrows i, j from C and D to C t D, and if there
is an object X and arrows f, g from C, D to X, then there is an arrow k such that the
following diagram commutes :
X
f k g
C C tD D
i j
Fig. 2: Commutative diagram for disjunction
The diagram in Figure 2 can be rephrased as follows:
C −→ C t D and D −→ C t D (1)
∀X, C −→ X and D −→ X =⇒ C t D −→ X (2)
Intuitively speaking, Arrows (1) and (2) tell us that C t D is the “smallest” object
which is “greater” than C and D.
Lemma 1. The category-theorectical semantics of C t D characterized by Definition 3
is compatible with the set-theoretical semantics of C t D, that means if h∆I , ·I i is an
interpretation under set-theoretical semantics, then the following holds:
(C t D)I = C I ∪ DI iff
C I ⊆ (C t D)I , DI ⊆ (C t D)I (3)
I I I I
∀X ⊆ ∆ , C ⊆ X, D ⊆ X =⇒ (C t D) ⊆ X (4)
Proof. “⇐=”. Due to (3) we have C I ∪ DI ⊆ (C t D)I . Let X = C I ∪ DI . Due to
(4) we have (C t D)I ⊆ X = C I ∪ DI .
“=⇒”. From (C tD)I = C I ∪DI , we have (3). Let x ∈ (C tD)I . Due to (C tD)I =
C I ∪ DI , we have x ∈ C I or x ∈ DI . Hence, x ∈ X since C I ⊆ X and DI ⊆ X.
At first glance, one can follow the same idea used in Definition 3 to define category-
theoretical semantics of C u D as described in Figure 3. This tells us that C u D is the
“greatest” object which is “smaller” than C and D.
X
f k g
C C uD D
i j
Fig. 3: Commutative diagram for a weak conjunction
However, such a definition is not sufficiently strong in order that the distributive
property of conjunction over disjunction is ensured. Hence, we need a stronger defini-
tion for conjunction.
Definition 4 (Category-theoretical semantics of conjunction). Let C, D, E, CuD, Cu
E, D t E and (C u D) t (C u E) be objects of Cc . Category-theoretical semantics of
C u D is defined by using the following arrows in Cc .
C u D −→ C and C u D −→ D (5)
∀X, X −→ C and X −→ D t E =⇒ X −→ (C u D) t (C u E) (6)
We prove that Definition 4 implies the weak definition of conjunction given in Fig-
ure 3 and the distributive property of conjunction over disjunction.
Lemma 2. The following arrows hold.
∀X, X −→ C and X −→ D =⇒ X −→ C u D (7)
C u (D t E) −→ (C u D) t (C u E) (8)
The following example describes a category which verifies all arrows from (3) to (5)
and (7), but not (8). This shows that the weak definition of conjunction with Arrows (5)
and (7) does not imply Arrow (8) (distributivity).
Example 2. For the sake of brevity, we rename the objects such as arrived, filled-room,
starting, started, finished introduced in Example 1 to I, F, S, D,T respectively. We can
check that these objects and arrows with identity arrows form a category where I and T
are initial and terminal objects. From Definition 3 and 4, we obtain (i) D t S ← −−
−−
→ T,
←−− ← −− ← −− ←− −
and thus F u (D t S) −−→ F u T −−→ F; (ii) F u D −−→ I, F u S −−→ I, and thus
(F u D) t (F u S) ← −−
−−
→ I. Since there does not exist F −→ I in this category, the
distributive property does not hold.
Lemma 3. The category-theorectical semantics of C u D characterized by Definition 4
is compatible with the set-theoretical semantics of C u D, that means if h∆I , ·I i is an
interpretation under set-theoretical semantics, then the following holds:
(C u D)I = C I ∩ DI , (C u E)I = C I ∩ E I iff
(C u D)I ⊆ C I , (C u D)I ⊆ DI (9)
I I I I
(C u E) ⊆ C , (C u E) ⊆ E (10)
I I I I
∀X ⊆ ∆ , X ⊆ C , X ⊆ (D t E) =⇒ X ⊆ ((C u D) t (C u E)) (11)
Proof. “⇐=”. Due to (9) we have (C u D)I ⊆ C I ∩ DI . Let X ⊆ ∆I such that
X = C I ∩ DI . This implies that X ⊆ C I and X ⊆ (D t ⊥)I . Due to (11) and
Lemma 1, we have X ⊆ ((C u D) t (C u ⊥))I = (C u D)I ∪ (C u ⊥)I . Moreover,
we have (C u ⊥)I = ∅ by (9). Thus, we obtain X ⊆ (C u D)I . Analogously, we can
show X ⊆ (C u E)I if X = C I ∩ E I .
“=⇒”. From (CuD)I = C I ∩DI and (CuE)I = C I ∩E I , we obtain (9) and (10). Let
x ∈ X I with X ⊆ C I and X ⊆ (D t E)I . Due to Lemma 1, (D t E)I = DI ∪ E I .
Again by Lemma 1, we have ((C u D) t (C u E))I = (C u D)I ∪ (C u E)I . If
x ∈ C I and x ∈ DI , then x ∈ C I ∩ DI = (C u D)I . If x ∈ C I and x ∈ E I , then
x ∈ C I ∩ E I = (C u E)I . Hence, (11) is proved.
With disjunction and conjunction, one can use the arrows C u ¬C −→ ⊥ and
> −→ C t ¬C to define category-theoretical semantics of negation. However, such a
definition does not allow to entail useful properties (c.f. Lemma 5) which are available
under set-theoretical semantics. Indeed, the following example shows that C ←−−−−
→ ¬¬C
cannot be entailed by C u ¬C −→ ⊥ and > −→ C t ¬C.
Example 3. We consider the category presented in Example 2. We have F u S −→ I
and T −→ F t S. Hence, we can put ¬F = S. Moreover, we have D u S −→ I and
T −→ D t S. Hence, we can put ¬S = D, and thus ¬¬F = D. However, there does not
exist F ←
−−
−−
→ D in this category.
Definition 5 (Category-theoretical semantics of negation). Let C, ¬C, C u ¬C, C t
¬C be objects of Cc . Category-theoretical semantics of ¬C is defined by using the
following arrows in Cc .
C u ¬C −→ ⊥ (12)
> −→ C t ¬C (13)
∀X, C u X −→ ⊥ =⇒ X −→ ¬C (14)
∀X, > −→ C t X =⇒ ¬C −→ X (15)
Lemma 4. The category-theorectical semantics of ¬C characterized by Definition 5
is compatible with the set-theoretical semantics of ¬C, that means if h∆I , ·I i is an
interpretation under set-theoretical semantics, then the following holds:
C I ∩ ¬C I ⊆ ⊥I and >I ⊆ C I ∪ ¬C I imply
∀X, (C u X)I ⊆ ⊥I =⇒ X I ⊆ (¬C)I (16)
I I I I
∀X, > ⊆ (C t X) =⇒ (¬C) ⊆ X (17)
Note that the properties C I ∩ ¬C I ⊆ ⊥I and >I ⊆ C I ∪ ¬C I suffice to characterize
the semantics of negation under set-theoretical semantics.
Proof. Let x ∈ X I with (C uX)I ⊆ ⊥I . Due to Lemma 3, we have (C uX)I = C I ∩
X I . Therefore, x ∈
/ C I , and thus x ∈ (¬C)I . Let x ∈ (¬C)I with >I ⊆ (C t X)I .
Hence, x ∈/ C . Due to Lemma 1, we have (C t X)I = C I ∪ X I . Thus, x ∈ X I .
I
Thanks to Properties (12-15), we obtain De Morgan’s laws and other properties for
category-theoretical semantics as follows.
Lemma 5. The following arrows hold.
C←
−−
−−
→ ¬¬C (18)
C −→ ¬D =⇒ D −→ ¬C (19)
C u D −→ ⊥ ⇐⇒ C −→ ¬D, D −→ ¬C (20)
¬(C u D) ←
−−
−−
→ ¬C t ¬D (21)
¬(C t D) ←
−−
−−
→ ¬C u ¬D (22)
In order to define category-theoretical semantics of existential restrictions, we need
to introduce new objects and arrows to Cc and Cr as described in Figure 4.
k l
R0 R R(∃R.C)
cod cod
dom dom
cod(R0 ) C cod(R(∃R.C) )
i j
m
dom(R0 ) dom(R(∃R.C) )
Fig. 4: Commutative diagram for existential restriction
Definition 6 (Category-theoretical semantics of existential restriction). Let ∃R.C, C
be objects of Cc , and R, R(∃R.C) be objects of Cr . Category-theoretical semantics of
∃R.C is defined by using arrows in Cc and Cr as follows. There is an arrow j from
cod(R(∃R.C) ) to C in Cc , an arrow l from R(∃R.C) to R in Cr , and if there is an object
R0 of Cr , an arrow k from R0 to R in Cr , and an arrow i from cod(R0 ) to C in Cc , then
there is an arrow m in Cc such that the diagram in Figure 4 commutes. The diagram in
Figure 4 can be rephrased as follows:
R(∃R.C) −→ R, cod(R(∃R.C) ) −→ C (23)
dom(R(∃R.C) ) ←
−−
−−
→ ∃R.C (24)
∀R0 , R0 −→ R, cod(R0 ) −→ C =⇒ dom(R0 ) −→ dom(R(∃R.C) ) (25)
Since dom(R(∃R.C) ) ← −−
−−
→ ∃R.C by (24), the objects dom(R(∃R.C) ) and ∃R.C are
mutually replaceable in the category context.
Lemma 6. The category-theorectical semantics of ∃R.C characterized by Definition 6
is compatible with the set-theoretical semantics of ∃R.C, that means if h∆I , ·I i is an
interpretation under set-theoretical semantics such that
I
R(∃R.C) ⊆ RI (26)
cod(R(∃R.C) )I ⊆ C I (27)
then the following holds:
dom(R(∃R.C) )I = {x ∈ ∆I | ∃y ∈ ∆I : hx, yi ∈ RI ∧ y ∈ C I } iff
∀R0 ⊆ ∆I × ∆I , R0 ⊆ RI , cod(R0 ) ⊆ C I =⇒ dom(R0 ) ⊆ dom(R(∃R.C) )I (28)
Proof. “⇐=”. Let x0 ∈ dom(R(∃R.C) )I . There is an element y ∈ cod(R(∃R.C) )I such
that hx0 , yi ∈ R(∃R.C)
I
by definition. Due to (27), we have y ∈ C I . Analogously, due to
(26), we have hx0 , yi ∈ RI . Thus, x0 ∈ {x ∈ ∆I | ∃y ∈ ∆I : hx, yi ∈ RI ∧ y ∈ C I }.
Let x0 ∈ {x ∈ ∆I | ∃y ∈ ∆I : hx, yi ∈ RI ∧ y ∈ C I }. By the set-theoretical
semantics, there is an element y ∈ C I such that hx0 , yi ∈ RI . Take an R0 ⊆ ∆I × ∆I
such that R0 ⊆ RI , cod(R0 ) ⊆ C I with x0 ∈ dom(R0 ) and y ∈ cod(R0 ). Due to (28),
we have x0 ∈ dom(R(∃R.C) )I .
“=⇒”. Let R0 ⊆ ∆I × ∆I such that R0 ⊆ RI , cod(R0 ) ⊆ C I . Let x0 ∈ dom(R0 ).
This implies that there is some y ∈ cod(R0 ) such that hx0 , yi ∈ R0 . Hence, y ∈ C I
and hx0 , yi ∈ RI . Therefore, x0 ∈ {x ∈ ∆I | ∃y ∈ ∆I : hx, yi ∈ RI ∧ y ∈ C I } =
dom(R(∃R.C) )I .
Lemma 7. The following properties hold:
C −→ ⊥ =⇒ ∃R.C −→ ⊥ (29)
C −→ D =⇒ ∃R.C −→ ∃R.D (30)
∃R.(C t D) ←
−−
−−
→ ∃R.C t ∃R.D (31)
The set-theoretical semantics of universal restriction can be defined as negation of ex-
istential restriction. However, the definition ∀R.C ← −−−−
→ ¬∃R.¬C does not allow to
obtain usual connections between existential and universal restrictions such as ∃R.D u
∀R.C −→ ∃R.(D u C). Therefore, we need more arrows to characterize the category-
theoretical semantics of universal restriction.
Definition 7 (Category-theoretical semantics of universal restriction). Let ∀R.C, C
be objects of Cc , and R be an object of Cr . Category-theoretical semantics of ∀R.C is
defined by using arrows in Cc and Cr as follows.
∀R.C ←
−−
−−
→ ¬∃R.¬C (32)
0 0 0 0
∀R , R −→ R, dom(R ) −→ ∀R.C =⇒ cod(R ) −→ C (33)
Lemma 8. The category-theoretical semantics of ∀R.C characterized by Definition 7
is compatible with the set-theoretical semantics of ∀R.C, that means if h∆I , ·I i is an
interpretation under set-theoretical semantics, then the following holds:
∀R.C I = {x ∈ ∆I | hx, yi ∈ RI =⇒ y ∈ C I } iff
∀R.C I = (¬∃R.¬C)I (34)
0 I I 0 I 0 I 0 I I
∀R ⊆ ∆ × ∆ , R ⊆ R , dom(R ) ⊆ ∀R.C =⇒ cod(R ) ⊆ C (35)
Proof. “⇐=”. We have {x ∈ ∆I | hx, yi ∈ RI =⇒ y ∈ C I } is the complement
of {x ∈ ∆I | ∃y ∈ ∆I : hx, yi ∈ RI ∧ y ∈ ¬C I } = ∃R.¬C I . Hence, we have
∀R.C I = {x ∈ ∆I | hx, yi ∈ RI =⇒ y ∈ C I } from (34).
“=⇒”. Let R0 ⊆ RI with dom(R0 ) ⊆ ∀R.C I . Let y ∈ cod(R0 ). There is some
I
x0 ∈ dom(R0 ) such that hx0 , yi ∈ R0 . Since R0 ⊆ RI and dom(R0 ) ⊆ ∀R.C I , we
have x ∈ ∀R.C I and hx0 , yi ∈ RI . By hypothesis, y ∈ C I .
Lemma 9. The following properties hold.
∀R.C u ∃R.¬C −→ ⊥ (36)
C −→ D =⇒ ∀R.C −→ ∀R.D (37)
∀R.(C u D) ←
−−
−−
→ ∀R.C u ∀R.D (38)
∃R.D u ∀R.C −→ ∃R.(D u C) (39)
Lemma 10 (Arrow and subsumption). Let O be an ALC ontology with signature
hC, Ri. Let Cc be a syntax category built from hC, Ri. It holds that O |= X v Y
(under set-theoretical semantics) if X −→ Y is an arrow added to Cc by Definitions 3,
4, 5, 6 and 7, and Lemmas 2, 5, 7 and 9.
So far we have introduced syntax categories Cc and Cr from a signature composed of
concept and role names. We have also defined arrows in Cc and Cr for characterizing
category-theoretical semantics of all ALC constructors occurring in concept objects of
Cc . The following definition extends syntax categories in such a way that they admit
the axioms of an ALC ontology as arrows apart from those defined for the ALC con-
structors.
Definition 8 (Ontology categories). Let C be an ALC concept and O an ALC ontol-
ogy from a signature hC, Ri. We define a concept ontology category Cc hC, Oi and a
role ontology category Cr hC, Oi as follows:
1. Cc hC, Oi and Cr hC, Oi are syntax categories from hC, Ri.
2. C is an object of Cc hC, Oi.
3. If E v F is an axiom in O, then ¬E t F is an object of Cc hC, Oi and there is an
arrow > −→ ¬E t F in Cc hC, Oi.
Note that both Cc hC, Oi and Cr hC, Oi may consist of more objects and arrows than
those introduced by Definitions (3-7) and Lemmas 2, 5, 7 and 9. We now introduce
category-theoretical satisfiability of an ALC concept with respect to an ALC ontology.
Definition 9. Let C be an ALC concept, O an ALC ontology. C is category-theoretically
unsatifiable with respect to O if there is an ontology category Cc hC, Oi which consists
of the arrow C −→ ⊥.
Since an ontology category Cc hC, Oi may consist of objects arbitrarily built from
the signature, Definition 9 offers possibilities to build a large Cc hC, Oi from which new
arrows can be discovered by applying arrows given in Definitions (3-7).
Theorem 1. Let O be an ALC ontology and C an ALC concept. C is category-theoreti-
cally unsatifiable with respect to O iff C is set-theoretically unsatifiable.
To prove this theorem, we need the following preliminary result.
Lemma 11. Let O be an ALC ontology and C an ALC concept. If C is set-theoretically
unsatifiable with respect to O then C is category-theoretically unsatifiable.
In order to prove this lemma, we use a tableau algorithm to generate from a un-
satisfiable ALC concept with respect to an ontology a set of completion trees each of
which contains a clash (⊥ or a pair {A, ¬A} where A is a concept name). To ensure
self-containedness of the paper, we describe here necessary elements which allow to
follow the proof of the lemma. We refer the readers to [9,10] for formal details.
We use sub(C, O) to denote a set of subconcepts in NNF (i.e. negations appear
only in front of concept name) from C and O. This set can be built by applying the
following rules :(i) C ∈ sub(C, O) and ¬E t F ∈ sub(C, O) for each axiom E v F ;
(ii) if ¬C ∈ sub(C, O) then C ∈ sub(C, O); (iii) if C u D or C t D ∈ sub(C, O)
then C, D ∈ sub(C, O); (iv) if ∃R.C or ∀R.C ∈ sub(C, O) then C ∈ sub(C, O). A
completion tree T = hv0 , V, E, Li is a tree where V is a set of nodes, and each node
x ∈ V is labelled with L(x) ⊆ sub(C, O), and a root v0 ∈ V with C ∈ L(v0 ); E
is a set of edges, and each edge hx, yi ∈ E is labelled with a role Lhx, yi = {R}. In
a completion tree T , a node x is blocked by an ancestor y if L(x) = L(y). To build
completion trees, a tableau algorithm starts by initializing a tree T0 and applies the
following completion rules to each clash-free tree T : [v-rule] for each axiom E v F
and each node x, ¬E t F ∈ L(x); [u-rule] if E u F ∈ L(x) then E, F ∈ L(x);
[t-rule] if E t F ∈ L(x) and {E, F } ∩ L(x) = ∅ then it creates two copies T1 and
T2 of the current tree T , and set L(x1 ) ← L(x1 ) ∪ {E}, L(x2 ) ← L(x2 ) ∪ {F }
where xi in Ti is a copy of x from T . [∃-rule] if ∃R.C ∈ L(x), x is not blocked and
x has no edge hx, x0 i with L(hx, x0 i = {R} then it creates a successor x0 of x, and set
L(x0 ) ← {C}, L(hx, x0 i ← {R}; [∀-rule] if ∀R.C ∈ L(x) and x has a successor x0
with L(hx, x0 i = {R} then it adds C to L(x0 ).
When [t-rule] is applied to a node x of a completion tree T with E t F ∈ L(x), it
generates two children trees T1 and T2 with a node x1 in T1 such that E tF, E ∈ L(x1 ),
and a node x2 in T2 such that E t F, F ∈ L(x2 ) as described above. In this case, we
say that T is parent of T1 and T2 by x; or T1 and T2 are children of T by x; x is called a
disjunction node by E tF ; and x1 , x2 are called disjunct nodes of x by E tF . We use T
to denote the tree whose nodes are completion trees generated by the tableau algorithm
as described above. A completion tree is complete if no completion rule is applicable. It
was shown that if C is set-theoretically unsatisfiable with respect to O then all complete
completion trees contain a clash (an incomplete completion tree may contain a clash)
[9,10]. Since this result does not depend on the order of applying completion rules to
nodes, we can assume in this proof that the following order [v-rule], [u-rule], [∀-
rule], [∃-rule] and [t-rule] is used, and a completion rule should be applied to the
most ancestor node if applicable. Some properties are drawn from this assumption.
(P1) If a node x of a completion tree T contains a clash then x is a leaf node of T .
(P2) For a completion tree T , if a node y is an ancestor of a node x in T such that x, y
are disjunction nodes, then the children trees by y are ancestors of the children
trees by x in T.
Proof of Lemma 11. We define an ontology category Cc hC, Oi from T by starting
from leafdtrees of T. By (P1), each leaf tree T dof T contains a clash in a leaf node y.
We have Y ∈L(y) Y −→ ⊥. We add an object Y ∈L(y) Y to Cc hC, Oi with the arrow.
d
In the sequel, we try to define a sequence of arrows started with Y ∈L(y) Y −→ ⊥
which makes clashes propagate from the leaves into the root of T. This propagation
has to get through two crucial kinds of passing: from a node of a completion tree to an
ancestor that is a disjunct node; and from such a disjunct node in a completion tree to
its disjunction node in the parent completion tree in T.
Let T1 and T2 be two leaf trees of T whose parent is T , and y1 , y2 two leaf nodes
of T1 , T2 containing a clash. By construction, Ti has a disjunct node xi which is an
ancestor of yi with xi 6= yi , and there is no disjunct node between xi and yi (among
descendants of xi ). For each node z between yi and xi if it exists, we define an object
add it to Cc hC, Oi. Let z 0 be the parent node of yi . There is a concept
d
Z∈L(z) Z and
∃R.D ∈ L(z ) and D ∈ L(yi ). In addition, if ∀R.D1 ∈ L(z 0 ) and [∀-rule] is applied to
0
z 0 then D1 ∈ L(yi ). We show that D −→ Z or D1 −→ Z for each concept Z ∈ L(yi ).
By construction, [t-rule] is not applied to yi (and any node from xi to yi ). If Z =
¬E t F comes from an axiom E v F , then D −→ > −→ Z. If Z comes from some
Z u Z0 d then we have to have already D −→ 0
d Z u Z −→ Z or D1 −→ Z u Z −→ Z.
0
Hence, Y ∈L(yi ) Y −→ ⊥ implies D u ∀R.Di ∈L(z0 ) Di −→ ⊥. By (29) and (39), we
d d
obtain ∃R.D u ∀R.Di ∈L(z0 ) ∀R.Di −→ ⊥, and thus Z∈L(z0 ) Z −→ ⊥. By using
d d
the same argument, we obtain X∈L(xi ) X −→ ⊥. We add an object X∈L(xi ) X to
Cc hC, Oi with the arrow. We now show X∈L(x) X −→ ⊥ where x is the disjunction
d
node of xi , L(x) = Wd∪{E tF }, L(x1 ) = W ∪{EdtF, E}, L(x2 ) = W d ∪{E tF, F }.
Due to (8), we have
d V ∈W V u (E t F ) −→ (
d V ∈W V u E) t d V ∈W V u F ).
(
Moreover, since X∈L(xi ) X −→ ⊥, we have ( V ∈W V u E) −→ ( V ∈W V u (E t
d
F ) u E −→ X∈L(x1 ) X −→ ⊥ (we have (E t F ) u E −→ E due to (1) and (7)), and
d d d
( V ∈W V u F ) −→ ( V ∈W V u (E t F ) u F −→ X∈L(x2 ) X −→ ⊥. Therefore,
d d
we obtain V ∈W V u(E tF ) −→ ⊥ due to (8), then add an object V ∈W V u(E tF )
to Cc hC, Oi with the arrow.
We can apply the same argument from x to the next disjunct node in T which is
an ancestor of x according to (P2), and go upwards in T to find itsdparent and sibling.
This process can continue and reach the root tree T0 of T. We get X∈L(x0 ) X −→ ⊥
where x0 is the root node of T0 . By construction, we have {C} ∪ {¬E t F | E v
F ∈ O} ⊆ L(x0 ). Let X ∈ L(x0 ). If X = ¬E t F for some axiom E v F ∈ O
then C −→ > −→ ¬E t F . Moreover, if X d = E or X = F with C = E u F
then C −→ E u F . This implies that C −→ X∈L(x0 ) X −→ ⊥. Hence, C −→ ⊥.
It is straightforward that Cc hC, Oi is an ontology category consisting of C −→ ⊥.
Moreover, an arrow > −→ ¬E u F is added to Cc hC, Oi for each axiom E v F . This
completes the proof of the lemma.
Proof of Theorem 1. “⇐=”. Let Cc hC, Oi be an ontology category. Assume that there
is an arrow C −→ ⊥ in Cc hC, Oi. Every arrow X −→ Y added to Cc hC, Oi must be
one of following cases: (i) X v Y is an axiom of O. Thus, O |= X v Y . (ii) X −→ Y
is added by Definitions 3, 4, 5, 6, 7. Due to Lemma 10, we have O |= X v Y . (iii)
X −→ Y is obtained by transitivity from X −→ Z and Z −→ Y . It holds that
O |= X v Z and O |= Z v Y imply O |= X v Y . Hence, if Cc hC, Oi consists of an
arrow C −→ ⊥, then O |= C v ⊥.
“=⇒”. A consequence of Lemma 11.
4 Conclusion and Future Work
We have presented a rewriting of the usual set-theoretical semantics of ALC by using
categorial language and showed that these two semantics are equivalent in the sense that
the problem of concept unsatisfiability is the same in both settings. Thanks to the mod-
ular representation of category-theoretical semantics composed of refined constraints,
one can identify and design interesting sublogics by removing some arrows from cate-
gorical definitions rather than an entire constructor. Such sublogics may necessitate new
reasoning procedures. We believe that category-theoretical semantics can be extended
to more expressive DLs with role constructors. For instance, role functionality can be
expressed as monic and epic arrows.
References
1. F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, P. F. Patel-Schneider (Eds.), The
Description Logic Handbook: Theory, Implementation and Applications, Second Edition,
Cambridge University Press, 2010.
2. P. Patel-Schneider, P. Hayes, I. Horrocks, Owl web ontology language semantics and abstract
syntax, in: W3C Recommendation, 2004.
3. B. Cuenca Grau, I. Horrocks, B. Motik, B. Parsia, P. Patel-Schneider, U. Sattler, Owl 2: The
next step for owl, journal of web semantics: Science, services and agents, World Wide Web
6 (2008) 309–322.
4. W. Lawvere, An elementary theory of the category of sets, in: Proc. Nat. Acad. Sci. (USA),
1964, p. 1506–1511.
5. R. Goldblatt, Topoi - The categorial analisys of logic, Mathematics, Dover publications,
2006.
6. D. I. Spivak, R. E. Kent, Ologs: a categorical framework for knowledge representation, PloS
one 7 (1) (2012) e24274.
7. C. Le Duc, Category-theoretical semantics of the description logic alc, in: Technical Report,
2021.
URL http://linc.iut.univ-paris8.fr/learningCafe/publicDocs/DL2021-TR.pdf
8. S. Mac Lane, I. Moerdijk, Sheaves in Geometry and Logic, Springer, 1992.
9. F. Baader, U. Sattler, Tableau algorithms for description logics, in: Proceedings of the In-
ternational Conference on Automated Reasoning with Tableaux and Related Methods, Vol.
1847, 2000, p. 118.
10. I. Horrocks, U. Sattler, A tableau decision procedure for SHOIQ, Journal Of Automated
Reasoning 39 (3) (2007) 249–276.