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, 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 arrived finished filled-room starting started 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 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 ¬C −→ ⊥ and −→ C ¬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.

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 D, C D, ¬C, ∃R.C, ∀R.C where C and D are ALC-concepts, and R is a role name in R. An axiom C 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 = ∆ 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 D) I = C I ∩ D I , (C D) I = C I ∪ D I (∃R.C) I = {x ∈ ∆ I | ∃y ∈ ∆ I , x, y ∈ R I ∧y ∈ C I } (∀R.C) I = {x ∈ ∆ I | ∀y ∈ ∆ I , x, y ∈ R I =⇒ y ∈ C I } An interpretation I satisfies a GCI C D if C I ⊆ D I . I

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 C c and a role syntax category C r from the signature C, R as follows:

1. Each object of C c is an ALC-concept built from C, R . In particular, ⊥ and are respectively initial and terminal objects, i. In this paper, an object of C c and C r is called concept and role object respectively. We transfer the vocabulary used in Description Logics to categories as follows. A concept object C D, C D or ¬C is respevtively called disjunction, conjunction and negation object. For an existential restriction object ∃R.C or universal restriction object ∀R.C, C is called the filler of ∃R.C and ∀R.C.

In the sequel, we introduce category-theoretical semantics of disjunction, conjunction, negation, existential and universal restriction objects by adding arrows to C c . 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 D be concept objects of C c . Category-theoretical semantics of C D is defined by using arrows in C c as follows. There are arrows i, j from C and D to C 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 D C D X i j f g k Fig. 2: Commutative diagram for disjunction

The diagram in Figure 2 can be rephrased as follows:

C −→ C D and D −→ C D (1) ∀X, C −→ X and D −→ X =⇒ C D −→ X(2)

Intuitively speaking, Arrows (1) and ( 2) tell us that C D is the "smallest" object which is "greater" than C and D.

Lemma 1. The category-theorectical semantics of C D characterized by Definition 3 is compatible with the set-theoretical semantics of C D, that means if ∆ I , • I is an interpretation under set-theoretical semantics, then the following holds:

(C D) I = C I ∪ D I iff C I ⊆ (C D) I , D I ⊆ (C D) I (3) ∀X ⊆ ∆ I , C I ⊆ X, D I ⊆ X =⇒ (C D) I ⊆ X(4)

Proof. "⇐=". Due to (3) we have

C I ∪ D I ⊆ (C D) I . Let X = C I ∪ D I . Due to (4) we have (C D) I ⊆ X = C I ∪ D I . "=⇒". From (C D) I = C I ∪D I , we have (3). Let x ∈ (C D) I . Due to (C D) I = C I ∪ D I , we have x ∈ C I or x ∈ D I . Hence, x ∈ X since C I ⊆ X and D I ⊆ X.

At first glance, one can follow the same idea used in Definition 3 to define categorytheoretical semantics of C D as described in Figure 3. This tells us that C D is the "greatest" object which is "smaller" than C and D.

C D −→ C and C D −→ D (5) ∀X, X −→ C and X −→ D E =⇒ X −→ (C D) (C E)(6)

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.

∀X, X −→ C and X −→ D =⇒ X −→ C D (7) C (D E) −→ (C D) (C 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 S ← − − − − → T, and thus Thanks to Properties (12-15), we obtain De Morgan's laws and other properties for category-theoretical semantics as follows.

F (D S) ← − − − − → F T ← − − − − → F; (ii) F D ← − − − − → I, F S ← − − − − → I,(C D) I = C I ∩ D I , (C E) I = C I ∩ E I iff (C D) I ⊆ C I , (C D) I ⊆ D I(9)(C E) I ⊆ C I , (C E) I ⊆ E I (10) ∀X ⊆ ∆ I , X ⊆ C I , X ⊆ (D E) I =⇒ X ⊆ ((C D) (C E)) I(C ¬C −→ ⊥ (12) −→ C ¬C (13) ∀X, C X −→ ⊥ =⇒ X −→ ¬C (14) ∀X, −→ C X =⇒ ¬C −→ X(

Lemma 5. The following arrows hold.

C ← − − − − → ¬¬C (18) C −→ ¬D =⇒ D −→ ¬C (19) C D −→ ⊥ ⇐⇒ C −→ ¬D, D −→ ¬C (20) ¬(C D) ← − − − − → ¬C ¬D (21) ¬(C D) ← − − − − → ¬C ¬D(22)

In order to define category-theoretical semantics of existential restrictions, we need to introduce new objects and arrows to C c and C r as described in Figure 4.

C cod(R ) cod(R (∃R.C) ) dom(R ) dom(R (∃R.C) ) R R (∃R.C) R i j cod codR (∃R.C) −→ R, cod(R (∃R.C) ) −→ C (23) dom(R (∃R.C) ) ← − − − − → ∃R.C (24) ∀R , R −→ R, cod(R ) −→ C =⇒ dom(R ) −→ 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 ∆ I , • I is an interpretation under set-theoretical semantics such that

R I (∃R.C) ⊆ R I (26) cod(R (∃R.C) ) I ⊆ C I (27)

then the following holds:

dom(R (∃R.C) ) I = {x ∈ ∆ I | ∃y ∈ ∆ I : x, y ∈ R I ∧ y ∈ C I } iff ∀R ⊆ ∆ I × ∆ I , R ⊆ R I , cod(R ) ⊆ C I =⇒ dom(R ) ⊆ dom(R (∃R.C) ) I(∈ C I such that x , y ∈ R I . Take an R ⊆ ∆ I × ∆ I such that R ⊆ R I , cod(R ) ⊆ C I with x ∈ dom(R ) and y ∈ cod(R ). Due to (28), we have x ∈ dom(R (∃R.C) ) I . "=⇒". Let R ⊆ ∆ I × ∆ I such that R ⊆ R I , cod(R ) ⊆ C I . Let x ∈ dom(R ).

This implies that there is some y ∈ cod(R ) such that x , y ∈ R . Hence, y ∈ C I and x , y ∈ R I . Therefore,

x ∈ {x ∈ ∆ I | ∃y ∈ ∆ I : x, y ∈ R I ∧ y ∈ C I } = dom(R (∃R.C) ) I .

∀R.C← − − − − → ¬∃R.¬C (32) ∀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 ∆ I , • I is an interpretation under set-theoretical semantics, then the following holds: So far we have introduced syntax categories C c and C r from a signature composed of concept and role names. We have also defined arrows in C c and C r for characterizing category-theoretical semantics of all ALC constructors occurring in concept objects of C c . 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.

∀R.C I = {x ∈ ∆ I | x, y ∈ R I =⇒ y ∈ C I } iff ∀R.C I = (¬∃R.¬C) I (34) ∀R ⊆ ∆ I × ∆ I , R ⊆ R I , dom(R ) ⊆ ∀R.C I =⇒ cod(R ) I ⊆ C I (35) Proof. "⇐=". We have {x ∈ ∆ I | x, y ∈ R I =⇒ y ∈ C I } is the complement of {x ∈ ∆ I | ∃y ∈ ∆ I : x, y ∈ R I ∧ y ∈ ¬C I } = ∃R.¬C I . Hence, we have ∀R.C I = {x ∈ ∆ I | x, y ∈ R I =⇒ y ∈ C I } from (34). "=⇒". Let R ⊆ R I with dom(R ) ⊆ ∀R.C I . Let y ∈ cod(R ). There is some x ∈ dom(R ) such that x , y ∈ R I . Since R ⊆ R I

Definition 8 (Ontology categories). Let C be an ALC concept and O an ALC ontology from a signature C, R . We define a concept ontology category C c C, O and a role ontology category C r C, O as follows: Since an ontology category C c C, O may consist of objects arbitrarily built from the signature, Definition 9 offers possibilities to build a large C c C, O from which new arrows can be discovered by applying arrows given in Definitions (3-7).

1. C c C, O and C r C, O are syntax categories from C, R . 2. C is an object of C c C, O . 3. If E F is an axiom in O, then ¬E F is an object of C c C, O

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 {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 F ∈ sub(C, O) for each axiom E F ; (ii) if ¬C ∈ sub(C, O) then C ∈ sub(C, O); (iii) if C D or C 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 = v 0 , V, E, L

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 v 0 ∈ V with C ∈ L(v 0 ); E is a set of edges, and each edge x, y ∈ E is labelled with a role L x, y = {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 T 0 and applies the following completion rules to each clash-free tree T : [ -rule] for each axiom E F and each node x, ¬E F ∈ L(x); [ -rule] if E F ∈ L(x) then E, F ∈ L(x); [ -rule] if E F ∈ L(x) and {E, F } ∩ L(x) = ∅ then it creates two copies T 1 and T 2 of the current tree T , and set L(x 1 ) ← L(x 1 ) ∪ {E}, L(x 2 ) ← L(x 2 ) ∪ {F } where x i in T i is a copy of x from T . [∃-rule] if ∃R.C ∈ L(x), x is not blocked and x has no edge x, x with L( x, x = {R} then it creates a successor x of x, and set L(x ) ← {C}, L( x, x ← {R}; [∀-rule] if ∀R.C ∈ L(x) and x has a successor x with L( x, x = {R} then it adds C to L(x ).

When [ -rule] is applied to a node x of a completion tree T with E F ∈ L(x), it generates two children trees T 1 and T 2 with a node x 1 in T 1 such that E F, E ∈ L(x 1 ), and a node x 2 in T 2 such that E F, F ∈ L(x 2 ) as described above. In this case, we say that T is parent of T 1 and T 2 by x; or T 1 and T 2 are children of T by x; x is called a disjunction node by E F ; and x 1 , x 2 are called disjunct nodes of x by E F . 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 [ -rule], [ -rule], [∀rule], [∃-rule] and [ -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 C c C, O 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 Y ∈L(y) Y −→ ⊥. We add an object Y ∈L(y) Y to C c C, O with the arrow.

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 T 1 and T 2 be two leaf trees of T whose parent is T , and y 1 , y 2 two leaf nodes of T 1 , T 2 containing a clash. By construction, T i has a disjunct node x i which is an ancestor of y i with x i = y i , and there is no disjunct node between x i and y i (among descendants of x i ). For each node z between y i and x i if it exists, we define an object Z∈L(z) Z and add it to C c C, O . Let z be the parent node of y i . There is a concept

∃R.D ∈ L(z ) and D ∈ L(y i ). In addition, if ∀R.D 1 ∈ L(z ) and [∀-rule] is applied to z then D 1 ∈ L(y i ). We show that D −→ Z or D 1 −→ Z for each concept Z ∈ L(y i ).

By construction, [ -rule] is not applied to y i (and any node from

x i to y i ). If Z = ¬E F comes from an axiom E F , then D −→ −→ Z. If Z comes from some Z Z then we have to have already D −→ Z Z −→ Z or D 1 −→ Z Z −→ Z.of x i , L(x) = W ∪{E F }, L(x 1 ) = W ∪{E F, E}, L(x 2 ) = W ∪{E F, F }. Due to (8), we have V ∈W V (E F ) −→ ( V ∈W V E) ( V ∈W V F ).

Moreover, since X∈L(xi) X −→ ⊥, we have ( V ∈W V E) −→ ( V ∈W V (E F ) E −→ X∈L(x1) X −→ ⊥ (we have (E F ) E −→ E due to (1) and ( 7)), and ( V ∈W V F ) −→ ( V ∈W V (E F ) F −→ X∈L(x2) X −→ ⊥. Therefore, we obtain V ∈W V (E F ) −→ ⊥ due to (8), then add an object V ∈W V (E F ) to C c C, O 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 T 0 of T. We get X∈L(x0) X −→ ⊥ where x 0 is the root node of T 0 . By construction, we have {C} ∪ {¬E F | E F ∈ O} ⊆ L(x 0 ). Let X ∈ L(x 0 ). If X = ¬E F for some axiom E

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.