Category-theoretical Semantics of the Description Logic ALC Chan Le Duc chan.leduc@univ-paris13.fr 0 Universite ́ Sorbonne Paris Nord, Laboratory in Medical Informatics and Knowledge Engineering in e-Health , LIMICS

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 propose in this paper a reformulation of the usual set-theoretical semantics of the description 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-theoretical semantics provides a more modular representation of the semantics of ALC and a new way to design algorithms for reasoning.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 smallest 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 replacing 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 formalism 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, lled-room, starting, started, nished; 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 License Attribution 4.0 International (CC BY 4.0) starting

started arrived nished of time-points. This might not be compatible with the semantics of subsumptions with set membership since, for instance a time-point in lled-room cannot belong to nished (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 related 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 settheoretical 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 category 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 unsatisfiable. This result allows us not only to employ objects and arrows to design reasoning procedures in the new setting, but also to identify interesting sublogics by removing/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, 9R:C, 8R: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 such that

I to each individual, and a subset of I I to each role name >I = I , ?I = ;, (:C)I = I n CI (C u D)I = CI \ DI , (C t D)I = CI [ DI (9R:C)I = fx 2 I j 9y 2 I ;hx; yi 2 RI ^y 2 CI g (8R:C)I = fx 2 I j 8y 2 I ; hx; yi 2 RI =) y 2 CI g

 An interpretation I satisfies a GCI C v D if CI DI . I is a model of O, written

I j= 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 CI 6= ;, and settheoretically unsatisfiable otherwise. We say that a GCI C v D is set-theoretically entailed by O, written O j= C v D, if CI 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 involve 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 objects 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(9R:C) defined for each object 9R: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 dom(R00) and cod(R) ! R0 ! R00 in Cr then there are arrows dom(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 concept object C t D, C u D or :C is respevtively called disjunction, conjunction and negation object. For an existential restriction object 9R:C or universal restriction object 8R:C, C is called the filler of 9R:C and 8R:C.

In the sequel, we introduce category-theoretical semantics of disjunction, conjunction, 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 semantics. 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 :

C f i k

X C t D g j

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 = CI [ DI iff

CI

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 definition 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 8X; X ! C and C u D ! C and X

! D ! D t E =) X ! (C u D) t (C u E)

We prove that Definition 4 implies the weak definition of conjunction given in Figure 3 and the distributive property of conjunction over disjunction.

Lemma 2. The following arrows hold.

8X; X C u (D t E) ! C and X

! D =) X ! (C u D) t (C u E) ! C u D

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, lled-room, starting, started, nished 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. ( 5 ) ( 6 ) ( 7 ) ( 8 ) (C u D)I (C u E)I 8X

CI ; (C u D)I CI ; (C u E)I

DI

EI

 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 = CI \ DI , (C u E)I = CI \ EI iff

I ; X

CI ; X (D t E)I =) X ((C u D) t (C u E))I Proof. “(=”. Due to ( 9 ) we have (C u D)I CI \ DI . Let X I such that X = CI \ DI . This implies that X CI 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 = CI \ EI . “=)”. From (CuD)I = CI \DI and (CuE)I = CI \EI , we obtain ( 9 ) and ( 10 ). Let x 2 XI with X CI and X (D t E)I . Due to Lemma 1, (D t E)I = DI [ EI . Again by Lemma 1, we have ((C u D) t (C u E))I = (C u D)I [ (C u E)I . If x 2 CI and x 2 DI , then x 2 CI \ DI = (C u D)I . If x 2 CI and x 2 EI , then x 2 CI \ EI = (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

! ? > ! C t :C 8X; C u X 8X; >

! ? =) X ! C t X =) :C ! :C ! X

 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:

 CI \ :CI ?I and >I CI [ :CI imply

8X; (C u X)I 8X; >I

?I =) XI (C t X)I =) (:C)I (:C)I Note that the properties CI \ :CI ?I and >I CI [ :CI suffice to characterize the semantics of negation under set-theoretical semantics.

Proof. Let x 2 XI with (C uX)I ?I . Due to Lemma 3, we have (C uX)I = CI \ XI . Therefore, x 2= CI , and thus x 2 (:C)I . Let x 2 (:C)I with >I (C t X)I . Hence, x 2= CI . Due to Lemma 1, we have (C t X)I = CI [ XI . Thus, x 2 XI .

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 C ! :D =) D C u D

! ? () C :(C u D) :(C t D) ! :C t :D ! :C u :D ! :C ! :D; D ! :C (18) (19) (20) (21) (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. dom dom R0

cod cod(R0) dom(R0) k i

R

C m j l

R(9R:C) cod cod(R(9R:C)) dom(R(9R:C)) Definition 6 (Category-theoretical semantics of existential restriction). Let 9R:C; C be objects of Cc, and R; R(9R:C) be objects of Cr. Category-theoretical semantics of

 9R:C is defined by using arrows in Cc and Cr as follows. There is an arrow j from

cod(R(9R:C)) to C in Cc, an arrow l from R(9R: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(9R:C) ! R; cod(R(9R:C))

! C dom(R(9R:C))

! 9R:C

Since dom(R(9R:C)) ! 9R:C by (24), the objects dom(R(9R:C)) and 9R:C are mutually replaceable in the category context. then the following holds:

R(I9R:C) cod(R(9R:C))I

RI

CI dom(R(9R:C))I = fx 2

I j 9y 2

I : hx; yi 2 RI ^ y 2 CI g iff 8R0

I Proof. “(=”. Let x0 2 dom(R(9R:C))I . There is an element y 2 cod(R(9R:C))I such that hx0; yi 2 R(I9R:C) by definition. Due to (27), we have y 2 CI . Analogously, due to (26), we have hx0; yi 2 RI . Thus, x0 2 fx 2 I j 9y 2 I : hx; yi 2 RI ^ y 2 CI g. Let x0 2 fx 2 I j 9y 2 I : hx; yi 2 RI ^ y 2 CI g. By the set-theoretical semantics, there is an element y 2 CI such that hx0; yi 2 RI . Take an R0 I I such that R0 RI , cod(R0) CI with x0 2 dom(R0) and y 2 cod(R0). Due to (28), we have x0 2 dom(R(9R:C))I . “=)”. Let R0 I I such that R0 RI , cod(R0) CI . Let x0 2 dom(R0). This implies that there is some y 2 cod(R0) such that hx0; yi 2 R0. Hence, y 2 CI and hx0; yi 2 RI . Therefore, x0 2 fx 2 I j 9y 2 I : hx; yi 2 RI ^ y 2 CI g = dom(R(9R:C))I .

Lemma 7. The following properties hold: Lemma 6. The category-theorectical semantics of 9R:C characterized by Definition 6 is compatible with the set-theoretical semantics of 9R:C, that means if h I ; I i is an interpretation under set-theoretical semantics such that (26) (27) (29) (30) (31) (32) (33) C ! ? =) 9R:C C ! D =) 9R:C 9R:(C t D) ! ? ! 9R:D ! 9R:C t 9R:D The set-theoretical semantics of universal restriction can be defined as negation of existential restriction. However, the definition 8R:C ! :9R::C does not allow to obtain usual connections between existential and universal restrictions such as 9R:D u 8R:C ! 9R:(D u C). Therefore, we need more arrows to characterize the categorytheoretical semantics of universal restriction.

Definition 7 (Category-theoretical semantics of universal restriction). Let 8R:C, C be objects of Cc, and R be an object of Cr. Category-theoretical semantics of 8R:C is defined by using arrows in Cc and Cr as follows.

8R:C 8R0; R0 ! :9R::C ! R; dom(R0) ! 8R:C =) cod(R0) ! C

 Lemma 8. The category-theoretical semantics of 8R:C characterized by Definition 7

is compatible with the set-theoretical semantics of 8R:C, that means if h I ; I i is an interpretation under set-theoretical semantics, then the following holds:

I j hx; yi 2 RI =) y 2 CI g iff 8R:CI = (:9R::C)I 8R0

I 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 j= 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 constructors.

Definition 8 (Ontology categories). Let C be an ALC concept and O an ALC ontology from a signature hC; Ri. We define a concept ontology category CchC; Oi and a role ontology category CrhC; Oi as follows:

 1. CchC; Oi and CrhC; Oi are syntax categories from hC; Ri. 2. C is an object of CchC; Oi. 3. If E v F is an axiom in O, then :E t F is an object of CchC; Oi and there is an arrow > ! :E t F in CchC; Oi.

Note that both CchC; Oi and CrhC; 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 CchC; Oi which consists of the arrow C ! ?. (34) (35) (36) (37) (38) (39)

Since an ontology category CchC; Oi may consist of objects arbitrarily built from the signature, Definition 9 offers possibilities to build a large CchC; 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-theoretically 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 unsatisfiable ALC concept with respect to an ontology a set of completion trees each of which contains a clash (? or a pair fA; :Ag 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 2 sub(C; O) and :E t F 2 sub(C; O) for each axiom E v F ; (ii) if :C 2 sub(C; O) then C 2 sub(C; O); (iii) if C u D or C t D 2 sub(C; O) then C; D 2 sub(C; O); (iv) if 9R:C or 8R:C 2 sub(C; O) then C 2 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 2 V is labelled with L(x) sub(C; O), and a root v0 2 V with C 2 L(v0); E is a set of edges, and each edge hx; yi 2 E is labelled with a role Lhx; yi = fRg. 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 2 L(x); [u-rule] if E u F 2 L(x) then E; F 2 L(x); [t-rule] if E t F 2 L(x) and fE; F g \ L(x) = ; then it creates two copies T1 and T2 of the current tree T , and set L(x1) L(x1) [ fEg, L(x2) L(x2) [ fF g where xi in Ti is a copy of x from T . [9-rule] if 9R:C 2 L(x), x is not blocked and x has no edge hx; x0i with L(hx; x0i = fRg then it creates a successor x0 of x, and set L(x0) fCg, L(hx; x0i fRg; [8-rule] if 8R:C 2 L(x) and x has a successor x0 with L(hx; x0i = fRg 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 2 L(x), it generates two children trees T1 and T2 with a node x1 in T1 such that E tF; E 2 L(x1), and a node x2 in T2 such that E t F; F 2 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], [8rule], [9-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 CchC; Oi from T by starting from leaf trees of T. By (P1), each leaf tree T of T contains a clash in a leaf node y. We have dY 2L(y) Y ! ?. We add an object dY 2L(y) Y to CchC; Oi with the arrow. In the sequel, we try to define a sequence of arrows started with dY 2L(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 dZ2L(z) Z and add it to CchC; Oi. Let z0 be the parent node of yi. There is a concept 9R:D 2 L(z0) and D 2 L(yi). In addition, if 8R:D1 2 L(z0) and [8-rule] is applied to z0 then D1 2 L(yi). We show that D ! Z or D1 ! Z for each concept Z 2 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 then we have to have already D ! Z u Z0 ! Z or D1 ! Z u Z0 ! Z. Hence, dY 2L(yi) Y ! ? implies D u d8R:Di2L(z0) Di ! ?. By (29) and (39), we obtain 9R:D u d8R:Di2L(z0) 8R:Di ! ?, and thus dZ2L(z0) Z ! ?. By using the same argument, we obtain dX2L(xi) X ! ?. We add an object dX2L(xi) X to CchC; Oi with the arrow. We now show dX2L(x) X ! ? where x is the disjunction node of xi, L(x) = W [fE tF g, L(x1) = W [fE tF; Eg, L(x2) = W [fE tF; F g. Due to ( 8 ), we have dV 2W V u (E t F ) ! (dV 2W V u E) t (dV 2W V u F ). Moreover, since dX2L(xi) X ! ?, we have (dV 2W V u E) ! (dV 2W V u (E t F ) u E ! dX2L(x1) X ! ? (we have (E t F ) u E ! E due to ( 1 ) and ( 7 )), and (dV 2W V u F ) ! (dV 2W V u (E t F ) u F ! dX2L(x2) X ! ?. Therefore, we obtain dV 2W V u(E tF ) ! ? due to ( 8 ), then add an object dV 2W V u(E tF ) to CchC; 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 its parent and sibling. This process can continue and reach the root tree T0 of T. We get dX2L(x0) X ! ? where x0 is the root node of T0. By construction, we have fCg [ f:E t F j E v F 2 Og L(x0). Let X 2 L(x0). If X = :E t F for some axiom E v F 2 O then C ! > ! :E t F . Moreover, if X = E or X = F with C = E u F then C ! E u F . This implies that C ! dX2L(x0) X ! ?. Hence, C ! ?. It is straightforward that CchC; Oi is an ontology category consisting of C ! ?. Moreover, an arrow > ! :E u F is added to CchC; Oi for each axiom E v F . This completes the proof of the lemma.

Proof of Theorem 1. “(=”. Let CchC; Oi be an ontology category. Assume that there is an arrow C ! ? in CchC; Oi. Every arrow X ! Y added to CchC; Oi must be one of following cases: (i) X v Y is an axiom of O. Thus, O j= X v Y . (ii) X ! Y is added by Definitions 3, 4, 5, 6, 7. Due to Lemma 10, we have O j= X v Y . (iii) X ! Y is obtained by transitivity from X ! Z and Z ! Y . It holds that O j= X v Z and O j= Z v Y imply O j= X v Y . Hence, if CchC; Oi consists of an arrow C ! ?, then O j= 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 modular representation of category-theoretical semantics composed of refined constraints, one can identify and design interesting sublogics by removing some arrows from categorical 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.

 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 International 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 .