11institutetext: Université Sorbonne Paris Nord, LIMICS, INSERM, U1142,
F-93000, Bobigny, France
11email<EMAIL_ADDRESS>
# Category-theoretical Semantics of the Description Logic $\mathcal{ALC}$
(extended version)

Chan Le Duc

###### 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 propose
in this paper a reformulation of the usual set-theoretical semantics of the
description logic $\mathcal{ALC}$ by using categorical language. In this
setting, $\mathcal{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 $\mathcal{ALC}$ and a new way
to design algorithms for reasoning. 111Copyright ©2021 for this paper by its
authors. Use permitted under Creative Commons License Attribution 4.0
International (CC BY 4.0)

##  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.
$\mathcal{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 $\mathcal{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 5 states of a meeting: $\mathsf{arrived}$,
$\mathsf{filled\mathchar 45\relax room}$, $\mathsf{starting}$,
$\mathsf{started}$, $\mathsf{finished}$; and a chronological order between
these states as depicted in Figure 1.

$\mathsf{arrived}$$\mathsf{finished}$$\mathsf{filled\mathchar 45\relax
room}$$\mathsf{starting}$$\mathsf{started}$ Figure 1: Objects and arrows for a
meeting

If we use concepts and subsumptions in $\mathcal{ALC}$ to represent the states
and order under set-theoretical semantics, then each such a concept should
represent a set of time-points. This might not be compatible with the
semantics of subsumptions with set membership since, for instance a time-point
in $\mathsf{filled\mathchar 45\relax room}$ cannot belong to
$\mathsf{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 $\mathcal{ALC}$, should be needed to infer the dashed relationship.
However, objects and arrows under category-theoretical semantics can be
straightforwardly used to present 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 $\mathcal{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 $\neg C$ by stating $C\sqcap\neg C\longrightarrow\bot$ and
$\top\longrightarrow C\sqcup\neg C$ because it is not possible to obtain
arrows such as $C\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\neg\neg C$ from this
definition. After providing category-theoretical semantics of each
constructor, unsatisfiability of an $\mathcal{ALC}$ concept $C$ with respect
to an ontology is reducible to the existence of a category consisting of an
arrow $C\longrightarrow\bot$. As a main result of the paper, we show that an
$\mathcal{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.

##  2 Syntax and set-theoretical semantics of $\mathcal{ALC}$

We present syntax and semantics of the Description Logic $\mathcal{ALC}$ [1]
with TBoxes and some basic inference problems.

######  Definition 1 (Syntax and set-theoretical semantics)

Let $\mathbf{R}$ and $\mathbf{C}$ be non-empty sets of _role names_ and
_concept names_ respectively. The set of $\mathcal{ALC}$-concepts is
inductively defined as the smallest set containing all concept names in
$\mathbf{C}$ with $\top$, $\bot$ and complex concepts that are inductively
defined as follows: $C\sqcap D$, $C\sqcup D$, $\neg C$, $\exists R.C$,
$\forall R.C$ where $C$ and $D$ are $\mathcal{ALC}$-concepts, and $R$ is a
role name in $\mathbf{R}$. An axiom $C\sqsubseteq D$ is called a general
concept inclusion (GCI) where $C,D$ are (possibly complex)
$\mathcal{ALC}$-concepts. An $\mathcal{ALC}$ ontology $\mathcal{O}$ is a
finite set of GCIs.

An interpretation ${\cal I}=\langle\Delta^{\cal{I}},\cdot^{\cal{I}}\rangle$
consists of a non-empty set $\Delta^{\cal{I}}$ (domain), and a function
$\cdot^{\cal{I}}$ (interpretation function) which associates a subset of
$\Delta^{\cal{I}}$ to each concept name, an element in $\Delta^{\mathcal{I}}$
to each individual, and a subset of $\Delta^{\cal{I}}\times\Delta^{\cal{I}}$
to each role name such that

$\top^{\cal{I}}$ | $=$ |  $\Delta^{\cal{I}}$, $\bot^{\cal I}=\emptyset$, $(\neg C)^{\cal I}=\Delta^{\cal{I}}\setminus C^{\cal I}$
---|---|---
$~{}(C\sqcap D)^{\cal I}$ | $=$ |  $C^{\cal I}\cap D^{\cal I}$, $(C\sqcup D)^{\cal I}=C^{\cal I}\cup D^{\cal I}$
$(\exists R.C)^{\cal I}$ | $=$ | $\\{x\\!\in\\!\Delta^{\cal{I}}\\!\mid\\!\exists y\\!\in\\!\Delta^{\cal{I}},\\!\langle x,y\rangle\\!\in\\!{R^{\cal I}}\\!\wedge\\!y\\!\in\\!C^{\cal I}\\}$
$(\forall R.C)^{\cal I}$ | $=$ | $\\{x\\!\in\\!\Delta^{\cal{I}}\\!\mid\\!\forall y\\!\in\\!\Delta^{\cal{I}},\langle x,y\rangle\\!\in\\!{R^{\cal I}}\\!\implies\\!y\\!\in\\!C^{\cal I}\\}$

An interpretation $\mathcal{I}$ satisfies a GCI $C\sqsubseteq D$ if $C^{\cal
I}\subseteq D^{\cal I}$. $\mathcal{I}$ is a model of $\mathcal{O}$, written
$\mathcal{I}\models\mathcal{O}$, if $\mathcal{I}$ satisfies each GCI in
$\mathcal{O}$.

In this case, we say that $\mathcal{O}$ is set-theoretically consistent, and
set-theoretically inconsistent otherwise. A concept $C$ is set-theoretically
satisfiable with respect to $\mathcal{O}$ if there is a model $\mathcal{I}$ of
$\mathcal{O}$ such that $C^{\mathcal{I}}\neq\emptyset$, and set-theoretically
unsatisfiable otherwise. We say that a GCI $C\sqsubseteq D$ is set-
theoretically entailed by $\mathcal{O}$, written $\mathcal{O}\models
C\sqsubseteq D$, if $C^{\mathcal{I}}\subseteq D^{\mathcal{I}}$ for all models
$\mathcal{I}$ of $\mathcal{O}$. The pair $\langle\mathbf{C},\mathbf{R}\rangle$
is called the signature of $\mathcal{O}$.

##  3 Category-theoretical semantics of $\mathcal{ALC}$

We can observe that the set-theoretical semantics of $\mathcal{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 $\mathcal{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, 7] on category theory for further information.

######  Definition 2 (Syntax categories)

Let $\mathbf{R}$ and $\mathbf{C}$ be non-empty sets of _role names_ and
_concept names_ respectively. We define a _concept syntax category_
$\mathscr{C}_{c}$ and a _role syntax category_ $\mathscr{C}_{r}$ from the
signature $\langle\mathbf{C},\mathbf{R}\rangle$ as follows:

  1. 1.

Each role name $R$ in $\mathbf{R}$ is an object $R$ of $\mathscr{C}_{r}$. In
particular, there are initial and terminal objects $R_{\bot}$ and $R_{\top}$
in $\mathscr{C}_{r}$ with arrows $R\longrightarrow R_{\top}$ and
$R_{\bot}\longrightarrow R$ for all object $R$ of $\mathscr{C}_{r}$. There is
also an identity arrow $R\longrightarrow R$ for each object $R$ of
$\mathscr{C}_{r}$.

  2. 2.

Each concept name in $\mathbf{C}$ is an object of $\mathscr{C}_{c}$. In
particular, $\bot$ and $\top$ are respectively initial and terminal objects,
i.e. there are arrows $C\longrightarrow\top$ and $\bot\longrightarrow C$ for
each object $C$ of $\mathscr{C}_{c}$. Furthermore, for each object $C$ of
$\mathscr{C}_{c}$ there is an identity arrow $C\longrightarrow C$, and for
each object $R$ of $\mathscr{C}_{r}$ there are two objects of
$\mathscr{C}_{c}$, namely $\mathsf{dom}(R)$ and $\mathsf{cod}(R)$.

  3. 3.

If there are arrows $E\longrightarrow F$ and $F\longrightarrow G$ in
$\mathscr{C}_{c}$ (resp. $\mathscr{C}_{r}$), then there is an arrow
$E\longrightarrow G$ in $\mathscr{C}_{c}$ (resp. $\mathscr{C}_{r}$).

  4. 4.

There are two functors $\mathsf{dom}$ and $\mathsf{cod}$ from
$\mathscr{C}_{r}$ to $\mathscr{C}_{c}$, i.e. they associate two objects
$\mathsf{dom}(R)$ and $\mathsf{cod}(R)$ of $\mathscr{C}_{c}$ to each object
$R$ of $\mathscr{C}_{r}$ such that

    1. (a)

$\mathsf{dom}(R_{\top})=\top$, $\mathsf{cod}(R_{\top})=\top$,
$\mathsf{dom}(R_{\bot})=\bot$ and $\mathsf{cod}(R_{\bot})=\bot$.

    2. (b)

if there is an arrow $R\longrightarrow R$ in $\mathscr{C}_{r}$ then there are
arrows $\mathsf{dom}(R)\longrightarrow\mathsf{dom}(R)$ and
$\mathsf{cod}(R)\longrightarrow\mathsf{cod}(R)$.

    3. (c)

if there are arrows $R\longrightarrow R^{\prime}\longrightarrow
R^{\prime\prime}$ in $\mathscr{C}_{r}$ then there are arrows
$\mathsf{dom}(R)\longrightarrow\mathsf{dom}(R^{\prime\prime})$ and
$\mathsf{cod}(R)\longrightarrow\mathsf{cod}(R^{\prime\prime})$.

    4. (d)

if there is an arrow $\mathsf{dom}(R)\longrightarrow\bot$ or
$\mathsf{cod}(R)\longrightarrow\bot$ in $\mathscr{C}_{c}$, then there is an
arrow $R\longrightarrow R_{\bot}$ in $\mathscr{C}_{r}$.

For each arrow $E\longrightarrow F$ in $\mathscr{C}_{c}$ or $\mathscr{C}_{r}$,
$E$ and $F$ are respectively called _domain_ and _codomain_ of the arrow.

Definition 3 provides a general framework with syntax elements and necessary
properties coming from category theory. We need to “instantiate” it to obtain
categories which include semantic constraints coming from axioms. The
following definition extends syntax categories in such a way that they admit
the axioms of an $\mathcal{ALC}$ ontology as arrows.

######  Definition 3 (Ontology categories)

Let $C_{0}$ be an $\mathcal{ALC}$ concept and $\mathcal{O}$ an $\mathcal{ALC}$
ontology from a signature $\langle\mathbf{C},\mathbf{R}\rangle$. We define a
_concept ontology category_ $\mathscr{C}_{c}\langle C_{0},\mathcal{O}\rangle$
and a _role ontology category_ $\mathscr{C}_{r}\langle
C_{0},\mathcal{O}\rangle$ as follows:

  1. 1.

$\mathscr{C}_{c}\langle C_{0},\mathcal{O}\rangle$ and $\mathscr{C}_{r}\langle
C_{0},\mathcal{O}\rangle$ are syntax categories from
$\langle\mathbf{C},\mathbf{R}\rangle$.

  2. 2.

$C_{0}$ is an object of $\mathscr{C}_{c}\langle C_{0},\mathcal{O}\rangle$.

  3. 3.

If $E\sqsubseteq F$ is an axiom of $\mathcal{O}$, then $\neg E\sqcup F$ is an
object of $\mathscr{C}_{c}\langle C_{0},\mathcal{O}\rangle$ and there is an
arrow $\top\longrightarrow\neg E\sqcup F$ in $\mathscr{C}_{c}\langle
C_{0},\mathcal{O}\rangle$.

In this paper, an object of $\mathscr{C}_{c}\langle C_{0},\mathcal{O}\rangle$
and $\mathscr{C}_{r}\langle C_{0},\mathcal{O}\rangle$ is called concept and
role object respectively. We transfer the vocabulary used in Description
Logics to categories as follows. A concept object $C\sqcup D$, $C\sqcap D$ or
$\neg C$ is respevtively called disjunction, conjunction and negation object.
For an existential restriction object $\exists R.C$ or universal restriction
object $\forall R.C$, $C$ is called the _filler_ of $\exists R.C$ and $\forall
R.C$.

In the sequel, we introduce category-theoretical semantics of disjunction,
conjunction, negation, existential and universal restriction objects if they
appear in $\mathscr{C}_{c}\langle C_{0},\mathcal{O}\rangle$. 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. Since semantics of an object in a category
depends to relationships with another ones, the following definitions need to
add to $\mathscr{C}_{c}\langle C_{0},\mathcal{O}\rangle$ and
$\mathscr{C}_{r}\langle C_{0},\mathcal{O}\rangle$ new objects and arrows.

######  Definition 4 (Category-theoretical semantics of disjunction)

Let $C,D,C\sqcup D$ be concept objects of $\mathscr{C}_{c}$. Category-
theoretical semantics of $C\sqcup D$ is defined by using arrows in
$\mathscr{C}_{c}$ as follows. There are arrows $i,j$ from $C$ and $D$ to
$C\sqcup 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\sqcup D$$C$$D$$X$${i}$${j}$${f}$${g}$${k}$ Figure 2: Commutative diagram
for disjunction

The diagram in Figure 2 can be rephrased as follows:

$\displaystyle C\longrightarrow C\sqcup D\text{ and }D\longrightarrow C\sqcup
D$ (1) $\displaystyle\forall X,C\longrightarrow X\text{ and }D\longrightarrow
X\Longrightarrow C\sqcup D\longrightarrow X$ (2)

Intuitively speaking, Arrows (1) and (2) tell us that $C\sqcup D$ is the
“smallest” object which is “greater” than $C$ and $D$.

###### Lemma 1

The category-theorectical semantics of $C\sqcup D$ characterized by Definition
4 is compatible with the set-theoretical semantics of $C\sqcup D$, that means
if $\langle\Delta^{\mathcal{I}},\cdot^{\mathcal{I}}\rangle$ is an
interpretation under set-theoretical semantics, then the following holds:

$(C\sqcup D)^{\mathcal{I}}=C^{\mathcal{I}}\cup D^{\mathcal{I}}$ iff

$\displaystyle C^{\mathcal{I}}\subseteq(C\sqcup
D)^{\mathcal{I}},D^{\mathcal{I}}\subseteq(C\sqcup D)^{\mathcal{I}}$ (3)
$\displaystyle\forall X\subseteq\Delta^{\mathcal{I}},C^{\mathcal{I}}\subseteq
X,D^{\mathcal{I}}\subseteq X\Longrightarrow(C\sqcup D)^{\mathcal{I}}\subseteq
X$ (4)

###### Proof

“$\Longleftarrow$”. Due to (3) we have $C^{\mathcal{I}}\cup
D^{\mathcal{I}}\subseteq(C\sqcup D)^{\mathcal{I}}$. Let $X=C^{\mathcal{I}}\cup
D^{\mathcal{I}}$. Due to (4) we have $(C\sqcup D)^{\mathcal{I}}\subseteq
X=C^{\mathcal{I}}\cup D^{\mathcal{I}}$.

“$\Longrightarrow$”. From $(C\sqcup D)^{\mathcal{I}}=C^{\mathcal{I}}\cup
D^{\mathcal{I}}$, we have (3). Let $x\in(C\sqcup D)^{\mathcal{I}}$. Due to
$(C\sqcup D)^{\mathcal{I}}=C^{\mathcal{I}}\cup D^{\mathcal{I}}$, we have $x\in
C^{\mathcal{I}}$ or $x\in D^{\mathcal{I}}$. Hence, $x\in X$ since
$C^{\mathcal{I}}\subseteq X$ and $D^{\mathcal{I}}\subseteq X$. $\square$

At first glance, one can follow the same idea used in Definition 4 to define
category-theoretical semantics of $C\sqcap D$ as described in Figure 3. They
tell us that $C\sqcap D$ is the “greatest” object which is “smaller” than $C$
and $D$.

$C\sqcap D$$C$$D$$X$${i}$${j}$${f}$${g}$${k}$ Figure 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 definition for conjunction.

######  Definition 5 (Category-theoretical semantics of conjunction)

Let $C,D,E,C\sqcap D,C\sqcap E$, $D\sqcup E$, $C\sqcap(D\sqcup E)$ and
$(C\sqcap D)\sqcup(C\sqcap E)$ be objects of $\mathscr{C}_{c}\langle
C_{0},\mathcal{O}\rangle$. Category-theoretical semantics of $C\sqcap D$ is
defined by using the following arrows in $\mathscr{C}_{c}\langle
C_{0},\mathcal{O}\rangle$.

$\displaystyle C\sqcap D\longrightarrow C\text{ and }C\sqcap D\longrightarrow
D$ (5) $\displaystyle\forall X,X\longrightarrow C\text{ and }X\longrightarrow
D\Longrightarrow X\longrightarrow C\sqcap D$ (6) $\displaystyle
C\sqcap(D\sqcup E)\longrightarrow(C\sqcap D)\sqcup(C\sqcap E)$ (7)

Note that under the set-theoretical semantics the distributive property of
disjunction over conjunction is not _independent_ , i.e. it is a consequence
of the definitions of disjunction and conjunction. However, this does not hold
under the category-theoretical semantics. The following lemma provides the
connection between the usual set semantics of conjunction and the category-
theoretical one given in Definition 5. In this lemma, Properties (8-10) are
rewritings of Arrows (5-7) in set theory.

###### Lemma 2

The category-theorectical semantics of $C\sqcap D$ characterized by Definition
5 is compatible with the set-theoretical semantics of $C\sqcap D$, that means
if $\langle\Delta^{\mathcal{I}},\cdot^{\mathcal{I}}\rangle$ is an
interpretation under set-theoretical semantics, then the following holds:

$(U\sqcap V)^{\mathcal{I}}=U^{\mathcal{I}}\cap V^{\mathcal{I}}$ for all
concepts $U,V$ iff

$\displaystyle(C\sqcap D)^{\mathcal{I}}\subseteq C^{\mathcal{I}},(C\sqcap
D)^{\mathcal{I}}\subseteq D^{\mathcal{I}}$ (8) $\displaystyle\forall
X\subseteq\Delta^{\mathcal{I}},X\subseteq C^{\mathcal{I}},X\subseteq
D^{\mathcal{I}}\Longrightarrow X\subseteq(C\sqcap D)^{\mathcal{I}}$ (9)
$\displaystyle(C\sqcap(D\sqcup E))^{\mathcal{I}}\subseteq((C\sqcap
D)\sqcup(C\sqcap E))^{\mathcal{I}}$ (10) $\displaystyle\hskip
28.45274pt\text{for all concepts }C,D\text{ and }E.$

###### Proof

“$\Longleftarrow$”. Due to (8) we have $(U\sqcap V)^{\mathcal{I}}\subseteq
U^{\mathcal{I}}\cap V^{\mathcal{I}}$. Let $X\subseteq\Delta^{\mathcal{I}}$
such that $X=U^{\mathcal{I}}\cap V^{\mathcal{I}}$. This implies that
$X\subseteq U^{\mathcal{I}}$ and $X\subseteq V^{\mathcal{I}}$. Due to (9), we
have $X\subseteq(U\sqcap V)^{\mathcal{I}}$.

“$\Longrightarrow$”. From $(C\sqcap D)^{\mathcal{I}}=C^{\mathcal{I}}\cap
D^{\mathcal{I}}$ we obtain (8). Moreover, if $X\subseteq C^{\mathcal{I}}$ and
$X\subseteq D^{\mathcal{I}}$ then $X\subseteq C^{\mathcal{I}}\cap
D^{\mathcal{I}}=(C\sqcap D)^{\mathcal{I}}$ by the hypothesis. Thus, (9) is
proved. To prove (10), we use the hypothesis and the usual set-theoretical
semantics as follows: $(C\sqcap(D\sqcup
E))^{\mathcal{I}}=C^{\mathcal{I}}\cap(D\sqcup
E)^{\mathcal{I}}=C^{\mathcal{I}}\cap(D^{\mathcal{I}}\cup
E^{\mathcal{I}})=(C^{\mathcal{I}}\cap D^{\mathcal{I}})\cup(C^{\mathcal{I}}\cap
E^{\mathcal{I}})=(C\sqcap D)^{\mathcal{I}}\cup(C\sqcap
E)^{\mathcal{I}}=((C\sqcap D)\sqcup(C\sqcap E))^{\mathcal{I}}$.

With disjunction and conjunction, one can use the arrows $C\sqcap\neg
C\longrightarrow\bot$ and $\top\longrightarrow C\sqcup\neg C$ to define
category-theoretical semantics of negation. However, such a definition does
not allow to entail useful properties (c.f. Lemma 4) which are available under
the set-theoretical semantics. Therefore, it is required to use more
properties to characterize negation under the category-theoretical semantics.

The following example describes a category which verifies all arrows from (3)
to (5) and (6), but not (7). This shows that the weak definition of
conjunction with Arrows (5) and (6) does not allow to entail Arrow (7)
(distributivity).

$\mathsf{I}$$\mathsf{T}$$\mathsf{F}$$\mathsf{S}$$\mathsf{D}$$\mathsf{D}\sqcup\mathsf{S}$$\mathsf{F}\sqcap\mathsf{D}$$\mathsf{F}\sqcap\mathsf{S}$
Figure 4: Category for Example 2. Some arrows resulting from transitivity are
omitted.

###### Example 2

For the sake of brevity, we rename the objects introduced in Example 1 such as
$\mathsf{arrived}$, $\mathsf{filled\mathchar 45\relax room}$,
$\mathsf{starting}$, $\mathsf{started}$, $\mathsf{finished}$ to $\mathsf{I}$,
$\mathsf{F}$, $\mathsf{S}$, $\mathsf{D}$,$\mathsf{T}$ respectively. Figure 4
describes a category consisting of the objects and arrows from Example 1 with
new ones. In this category, the conjunctions and disjunction with the arrows
satisfy Definitions 4 and 5. We have
$\mathsf{D}\sqcup\mathsf{S}\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\mathsf{T}$, and thus
$\mathsf{F}\sqcap(\mathsf{D}\sqcup\mathsf{S})\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\mathsf{F}\sqcap\mathsf{T}\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\mathsf{F}$. Moreover,
we have $\mathsf{F}\sqcap\mathsf{D}\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\mathsf{I}$,
$\mathsf{F}\sqcap\mathsf{S}\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\mathsf{I}$, and thus
$(\mathsf{F}\sqcap\mathsf{D})\sqcup(\mathsf{F}\sqcap\mathsf{S})\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\mathsf{I}$. However,
since $\mathsf{F}\not\longrightarrow\mathsf{I}$, the distributive property
does not hold in this category.

With disjunction and conjunction, one can use the arrows $C\sqcap\neg
C\longrightarrow\bot$ and $\top\longrightarrow C\sqcup\neg C$ to define
category-theoretical semantics of negation. However, such a definition does
not allow to entail useful properties (c.f. Lemma 4) which are available under
the set-theoretical semantics. Therefore, it is required to use more
properties to characterize negation under category-theoretical semantics.
Indeed, the following example shows that $C\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\neg\neg C$ do not hold.

###### Example 3

We consider the category in Figure 5. We have
$\mathsf{F}\sqcap\mathsf{S}\longrightarrow\mathsf{I}$ and
$\mathsf{T}\longrightarrow\mathsf{F}\sqcup\mathsf{S}$. Hence, we can put
$\neg\mathsf{F}=\mathsf{S}$. Moreover, we have
$\mathsf{D}\sqcap\mathsf{S}\longrightarrow\mathsf{I}$ and
$\mathsf{T}\longrightarrow\mathsf{D}\sqcup\mathsf{S}$. Hence, we can put
$\neg\mathsf{S}=\mathsf{D}$, and thus $\neg\neg\mathsf{F}=\mathsf{D}$.
However, there does not exist the arrows $\mathsf{F}\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\mathsf{D}$ in this
category.

$\mathsf{I}$$\mathsf{T}$$\mathsf{F}$$\mathsf{S}$$\mathsf{D}$$\mathsf{D}\sqcup\mathsf{S}$$\mathsf{F}\sqcup\mathsf{S}$$\mathsf{D}\sqcap\mathsf{S}$$\mathsf{F}\sqcap\mathsf{S}$
Figure 5: Category for Example 3. Some arrows resulting from transitivity are
missing.

######  Definition 6 (Category-theoretical semantics of negation)

Let $C,\neg C,C\sqcap\neg C,C\sqcup\neg C$ be objects of $\mathscr{C}_{c}$.
Category-theoretical semantics of $\neg C$ is defined by using the following
arrows in $\mathscr{C}_{c}$.

$\displaystyle C\sqcap\neg C\longrightarrow\bot$ (11)
$\displaystyle\top\longrightarrow C\sqcup\neg C$ (12) $\displaystyle\forall
X,C\sqcap X\longrightarrow\bot\Longrightarrow X\longrightarrow\neg C$ (13)
$\displaystyle\forall X,\top\longrightarrow C\sqcup X\Longrightarrow\neg
C\longrightarrow X$ (14)

###### Lemma 3

The category-theorectical semantics of $\neg C$ characterized by Definition 6
is compatible with the set-theoretical semantics of $\neg C$, that means if
$\langle\Delta^{\mathcal{I}},\cdot^{\mathcal{I}}\rangle$ is an interpretation
under set-theoretical semantics, then the following holds:

$C^{\mathcal{I}}\cap\neg C^{\mathcal{I}}\subseteq\bot^{\mathcal{I}}$ and
$\top^{\mathcal{I}}\subseteq C^{\mathcal{I}}\cup\neg C^{\mathcal{I}}$ imply

$\displaystyle\forall X,(C\sqcap
X)^{\mathcal{I}}\subseteq\bot^{\mathcal{I}}\Longrightarrow
X^{\mathcal{I}}\subseteq(\neg C)^{\mathcal{I}}$ (15) $\displaystyle\forall
X,\top^{\mathcal{I}}\subseteq(C\sqcup X)^{\mathcal{I}}\Longrightarrow(\neg
C)^{\mathcal{I}}\subseteq X^{\mathcal{I}}$ (16)

Note that the properties $C^{\mathcal{I}}\cap\neg
C^{\mathcal{I}}\subseteq\bot^{\mathcal{I}}$ and $\top^{\mathcal{I}}\subseteq
C^{\mathcal{I}}\cup\neg C^{\mathcal{I}}$ suffice to characterize the semantics
of negation under the set-theoretical semantics.

###### Proof

Let $x\in X^{\mathcal{I}}$ with $(C\sqcap
X)^{\mathcal{I}}\subseteq\bot^{\mathcal{I}}$. Due to Lemma 2, we have
$(C\sqcap X)^{\mathcal{I}}=C^{\mathcal{I}}\cap X^{\mathcal{I}}$. Therefore,
$x\notin C^{\mathcal{I}}$, and thus $x\in(\neg C)^{\mathcal{I}}$. Let
$x\in(\neg C)^{\mathcal{I}}$ with $\top^{\mathcal{I}}\subseteq(C\sqcup
X)^{\mathcal{I}}$. Hence, $x\notin C^{\mathcal{I}}$. Due to Lemma 1, we have
$(C\sqcup X)^{\mathcal{I}}=C^{\mathcal{I}}\cup X^{\mathcal{I}}$. Therefore,
$x\in X^{\mathcal{I}}$. $\square$

Thanks to Properties (11-14), we obtain De Morgan’s laws and other properties
for category-theoretical semantics as follows.

###### Lemma 4

The following arrows hold.

$\displaystyle C\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\neg\neg C$ (23)
$\displaystyle C\longrightarrow\neg D\Longrightarrow D\longrightarrow\neg C$
(24) $\displaystyle C\sqcap D\longrightarrow\bot\Longleftrightarrow
C\longrightarrow\neg D,D\longrightarrow\neg C$ (25) $\displaystyle\neg(C\sqcap
D)\mathrel{\raise 3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\neg C\sqcup\neg D$ (32)
$\displaystyle\neg(C\sqcup D)\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\neg C\sqcap\neg D$ (39)

###### Proof

  1. 1.

By Properties (11) and (13) where $C$ gets $\neg C$ and $X$ gets $C$, we have
$C\longrightarrow\neg\neg C$. Analogously, by Properties (12) and (14), we
obtain $\neg\neg C\longrightarrow C$. Hence, (23) is proved.

  2. 2.

To prove (24), we need $C\sqcap D\longrightarrow\bot$ which follows from
$C\sqcap D\longrightarrow C\longrightarrow\neg D$ and $C\sqcap
D\longrightarrow D$, and thus $C\sqcap D\longrightarrow D\sqcap\neg
D\longrightarrow\bot$.

  3. 3.

To prove (25), we start by proving $C\longrightarrow\neg D\Longrightarrow
C\sqcap D\longrightarrow\bot$. We have $C\sqcap D\longrightarrow D$ and
$C\sqcap D\longrightarrow C\longrightarrow\neg D$. By definition of
conjunction, we obtain $C\sqcap D\longrightarrow D\sqcap\neg
D\longrightarrow\bot$. To prove the other direction, we use (13) with $X=D$ or
$X=C$.

  4. 4.

To prove (32), we need the definitions of conjunction, disjunction and
negation. We have $C\sqcap D\longrightarrow C$ and $C\sqcap D\longrightarrow
D$. Due to (24), we obtain $\neg C\longrightarrow\neg(C\sqcap D)$ and $\neg
D\longrightarrow\neg(C\sqcap D)$. By the definition of disjunction, we obtain
$\neg C\sqcup\neg D\longrightarrow\neg(C\sqcap D)$. To prove the inverse, we
take arrows $\neg C\longrightarrow\neg C\sqcup\neg D$ and $\neg
D\longrightarrow\neg C\sqcup\neg D$ from the definition of disjunction. Due to
(24), it follows that $\neg(\neg C\sqcup\neg D)\longrightarrow C$ and
$\neg(\neg C\sqcup\neg D)\longrightarrow D$. By Definition 5, we obtain
$\neg(\neg C\sqcup\neg D)\longrightarrow C\sqcap D$. Due to (24) and (23), it
follows that $\neg(C\sqcap D)\longrightarrow\neg C\sqcup\neg D$.

  5. 5.

Analogously, we can prove (39) by starting with arrows $\neg C\sqcap\neg
D\longrightarrow\neg C$ and $\neg C\sqcap\neg D\longrightarrow\neg D$ from the
definition of conjunction. Due to (24), we have $C\longrightarrow\neg(\neg
C\sqcap\neg D)$ and $D\longrightarrow\neg(\neg C\sqcap\neg D)$. By the
definition of disjunction, we have $C\sqcup D\longrightarrow\neg(\neg
C\sqcap\neg D)$, and by (24) we obtain $(\neg C\sqcap\neg
D)\longrightarrow\neg(C\sqcup D)$. To prove the inverse, we take arrows
$C\longrightarrow C\sqcup D$ and $D\longrightarrow C\sqcup D$ obtained from
the definition of disjunction. Due to (24), we have $\neg(C\sqcup
D)\longrightarrow\neg C$ and $\neg(C\sqcup D)\longrightarrow\neg D$. By
Definition 5, we have $\neg(C\sqcup D)\longrightarrow\neg C\sqcap\neg D$.
$\square$

In order to define category-theoretical semantics of existential restrictions,
we need to introduce new objects and arrows to $\mathscr{C}_{c}$ and
$\mathscr{C}_{r}$ as described in Figure 6.

$C$$\mathsf{cod}(R^{\prime})$$\mathsf{cod}(R_{(\exists
R.C)})$$\mathsf{dom}(R^{\prime})$$\mathsf{dom}(R_{(\exists
R.C)})$$R^{\prime}$$R_{(\exists
R.C)}$$R$${i}$${j}$$\mathsf{cod}$$\mathsf{cod}$${k}$${l}$$\mathsf{dom}$$\mathsf{dom}$$m$
Figure 6: Commutative diagram for existential restriction

######  Definition 7 (Category-theoretical semantics of existential
restriction)

Let $\exists R.C,C$ be objects of $\mathscr{C}_{c}$, and $R,R_{(\exists R.C)}$
be objects of $\mathscr{C}_{r}$. Category-theoretical semantics of $\exists
R.C$ is defined by using arrows in $\mathscr{C}_{c}$ and $\mathscr{C}_{r}$ as
follows. There is an arrow $j$ from $\mathsf{cod}(R_{(\exists R.C)})$ to $C$
in $\mathscr{C}_{c}$, an arrow $l$ from $R_{(\exists R.C)}$ to $R$ in
$\mathscr{C}_{r}$, and if there is an object $R^{\prime}$ of
$\mathscr{C}_{r}$, an arrow $k$ from $R^{\prime}$ to $R$ in $\mathscr{C}_{r}$,
and an arrow $i$ from $\mathsf{cod}(R^{\prime})$ to $C$ in $\mathscr{C}_{c}$,
then there is an arrow $m$ in $\mathscr{C}_{c}$ such that the diagram in
Figure 6 commutes.

The diagram in Figure 6 can be rephrased as follows:

$\displaystyle R_{(\exists R.C)}\longrightarrow R,\mathsf{cod}(R_{(\exists
R.C)})\longrightarrow C$ (40) $\displaystyle\mathsf{dom}(R_{(\exists
R.C)})\mathrel{\raise 3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\exists R.C$ (47)
$\displaystyle\forall R^{\prime},R^{\prime}\longrightarrow
R,\mathsf{cod}(R^{\prime})\longrightarrow
C\Longrightarrow\mathsf{dom}(R^{\prime})\longrightarrow\mathsf{dom}(R_{(\exists
R.C)})$ (48)

Since $\mathsf{dom}(R_{(\exists R.C)})\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\exists R.C$ by (47),
the objects $\mathsf{dom}(R_{(\exists R.C)})$ and $\exists R.C$ are mutually
replaceable in the category context.

###### Lemma 5

The category-theorectical semantics of $\exists R.C$ characterized by
Definition 7 is compatible with the set-theoretical semantics of $\exists
R.C$, that means if $\langle\Delta^{\mathcal{I}},\cdot^{\mathcal{I}}\rangle$
is an interpretation under set-theoretical semantics such that

$\displaystyle R_{(\exists R.C)}^{\mathcal{I}}\subseteq R^{\mathcal{I}}$ (49)
$\displaystyle\mathsf{cod}(R_{(\exists R.C)})^{\mathcal{I}}\subseteq
C^{\mathcal{I}}$ (50)

then the following holds:

$\mathsf{dom}(R_{(\exists
R.C)})^{\mathcal{I}}=\\{x\in\Delta^{\mathcal{I}}\mid\exists
y\in\Delta^{\mathcal{I}}\mathrel{\mathop{\mathchar 58\relax}}\langle
x,y\rangle\in R^{\mathcal{I}}\wedge y\in C^{\mathcal{I}}\\}$ iff

$\displaystyle\forall
R^{\prime}\subseteq\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}},{R^{\prime}}\subseteq
R^{\mathcal{I}},\mathsf{cod}(R^{\prime})\subseteq
C^{\mathcal{I}}\Longrightarrow\mathsf{dom}(R^{\prime})\subseteq\mathsf{dom}(R_{(\exists
R.C)})^{\mathcal{I}}$ (51)

###### Proof

“$\Longleftarrow$”. Let $x^{\prime}\in\mathsf{dom}(R_{(\exists
R.C)})^{\mathcal{I}}$. There is an element $y\in\mathsf{cod}(R_{(\exists
R.C)})^{\mathcal{I}}$ such that $\langle x^{\prime},y\rangle\in R_{(\exists
R.C)}^{\mathcal{I}}$ by definition. Due to (50), we have $y\in
C^{\mathcal{I}}$. Analogously, due to (49), we have $\langle
x^{\prime},y\rangle\in R^{\mathcal{I}}$. Thus,
$x^{\prime}\in\\{x\in\Delta^{\mathcal{I}}\mid\exists
y\in\Delta^{\mathcal{I}}\mathrel{\mathop{\mathchar 58\relax}}\langle
x,y\rangle\in R^{\mathcal{I}}\wedge y\in C^{\mathcal{I}}\\}$.

Let $x^{\prime}\in\\{x\in\Delta^{\mathcal{I}}\mid\exists
y\in\Delta^{\mathcal{I}}\mathrel{\mathop{\mathchar 58\relax}}\langle
x,y\rangle\in R^{\mathcal{I}}\wedge y\in C^{\mathcal{I}}\\}$. By the set-
theoretical semantics, there is an element $y\in C^{\mathcal{I}}$ such that
$\langle x^{\prime},y\rangle\in R^{\mathcal{I}}$. Take an
$R^{\prime}\subseteq\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}$ such that
$R^{\prime}\subseteq R^{\mathcal{I}}$, $\mathsf{cod}(R^{\prime})\subseteq
C^{\mathcal{I}}$ with $x^{\prime}\in\mathsf{dom}(R^{\prime})$ and
$y\in\mathsf{cod}(R^{\prime})$. Due to (51), we have
$x^{\prime}\in\mathsf{dom}(R_{(\exists R.C)})^{\mathcal{I}}$.

“$\Longrightarrow$”. Let
$R^{\prime}\subseteq\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}$ such that
$R^{\prime}\subseteq R^{\mathcal{I}}$, $\mathsf{cod}(R^{\prime})\subseteq
C^{\mathcal{I}}$. Let $x^{\prime}\in\mathsf{dom}(R^{\prime})$. This implies
that there is some $y\in\mathsf{cod}(R^{\prime})$ such that $\langle
x^{\prime},y\rangle\in R^{\prime}$. Hence, $y\in C^{\mathcal{I}}$ and $\langle
x^{\prime},y\rangle\in R^{\mathcal{I}}$. Therefore,
$x^{\prime}\in\\{x\in\Delta^{\mathcal{I}}\mid\exists
y\in\Delta^{\mathcal{I}}\mathrel{\mathop{\mathchar 58\relax}}\langle
x,y\rangle\in R^{\mathcal{I}}\wedge y\in C^{\mathcal{I}}\\}$ $=$
$\mathsf{dom}(R_{(\exists R.C)})^{\mathcal{I}}$. $\square$

###### Lemma 6

The following properties hold:

$\displaystyle C\longrightarrow\bot\Longrightarrow\exists
R.C\longrightarrow\bot$ (52) $\displaystyle C\longrightarrow
D\Longrightarrow\exists R.C\longrightarrow\exists R.D$ (53)

###### Proof

  1. 1.

We have $\mathsf{cod}(R_{(\exists R.C)})\longrightarrow C$ by definition. By
hypothesis $C\longrightarrow\bot$, we have $\mathsf{cod}(R_{(\exists
R.C)})\longrightarrow\bot$ due Definition 2 of $\mathsf{cod}$. Again, due
Definition 2 of $\mathsf{cod}$, we have $R_{(\exists R.C)}\longrightarrow
R_{\bot}$. Moreover, we have $\mathsf{dom}(R_{(\exists
R.C)})\longrightarrow\bot$ due Definition 2 of $\mathsf{dom}$. By Definition
7, we obtain $\exists R.C\longrightarrow\bot$.

  2. 2.

To prove (53) we consider two objects $R_{(\exists R.C)}$ and $R_{(\exists
R.D)}$ in $\mathscr{C}_{r}$. We have $R_{(\exists R.C)}\longrightarrow R$ and
$\mathsf{cod}(R_{(\exists R.C)})\longrightarrow C\longrightarrow D$. By
definition, we obtain $\mathsf{dom}(R_{(\exists
R.C)})\longrightarrow\mathsf{dom}(R_{(\exists R.D)})$. $\square$

The set-theoretical semantics of universal restriction can be defined as
negation of existential restriction. However, the definition $\forall
R.C\mathrel{\raise 3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\neg\exists R.\neg C$
does not allow to obtain usual connections between existential and universal
restrictions such as $\exists R.D\sqcap\forall R.C\longrightarrow\exists
R.(D\sqcap C)$ under category-theoretical semantics. Therefore, we need more
arrows to define category-theoretical semantics of universal restriction as
follows.

######  Definition 8 (Category-theoretical semantics of universal restriction)

Let $\forall R.C$, $C$ be objects of $\mathscr{C}_{c}$, and $R$ be an object
of $\mathscr{C}_{r}$. Category-theoretical semantics of $\forall R.C$ is
defined by using arrows in $\mathscr{C}_{c}$ and $\mathscr{C}_{r}$ as follows.

$\displaystyle\forall R.C\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\neg\exists R.\neg C$
(60) $\displaystyle\forall R^{\prime},R^{\prime}\longrightarrow
R,\mathsf{dom}(R^{\prime})\longrightarrow\forall
R.C\Longrightarrow\mathsf{cod}(R^{\prime})\longrightarrow C$ (61)

###### Lemma 7

The category-theoretical semantics of $\forall R.C$ characterized by
Definition 8 is compatible with the set-theoretical semantics of $\forall
R.C$, that means if $\langle\Delta^{\mathcal{I}},\cdot^{\mathcal{I}}\rangle$
is an interpretation under set-theoretical semantics, then the following
holds:

$\forall R.C^{\mathcal{I}}=\\{x\in\Delta^{\mathcal{I}}\mid\langle
x,y\rangle\in R^{\mathcal{I}}\Longrightarrow y\in C^{\mathcal{I}}\\}$ iff

$\displaystyle\forall R.C^{\mathcal{I}}=(\neg\exists R.\neg C)^{\mathcal{I}}$
(62) $\displaystyle\forall
R^{\prime}\subseteq\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}},R^{\prime}\subseteq
R^{\mathcal{I}},\mathsf{dom}(R^{\prime})\subseteq\forall
R.C^{\mathcal{I}}\Longrightarrow\mathsf{cod}(R^{\prime})^{\mathcal{I}}\subseteq
C^{\mathcal{I}}$ (63)

###### Proof

“$\Longleftarrow$”. We have $\\{x\in\Delta^{\mathcal{I}}\mid\langle
x,y\rangle\in R^{\mathcal{I}}\Longrightarrow y\in C^{\mathcal{I}}\\}$ is the
complement of $\\{x\in\Delta^{\mathcal{I}}\mid\exists
y\in\Delta^{\mathcal{I}}\mathrel{\mathop{\mathchar 58\relax}}\langle
x,y\rangle\in R^{\mathcal{I}}\wedge y\in\neg C^{\mathcal{I}}\\}=\exists R.\neg
C^{\mathcal{I}}$. Hence, we have $\forall
R.C^{\mathcal{I}}=\\{x\in\Delta^{\mathcal{I}}\mid\langle x,y\rangle\in
R^{\mathcal{I}}\Longrightarrow y\in C^{\mathcal{I}}\\}$ from (62).

“$\Longrightarrow$”. Let $R^{\prime}\subseteq R^{\mathcal{I}}$ with
$\mathsf{dom}(R^{\prime})\subseteq\forall R.C^{\mathcal{I}}$. Let
$y\in\mathsf{cod}(R^{\prime})$. There is some
$x^{\prime}\in\mathsf{dom}(R^{\prime})$ such that $\langle
x^{\prime},y\rangle\in{R^{\prime}}^{\mathcal{I}}$. Since $R^{\prime}\subseteq
R^{\mathcal{I}}$ and $\mathsf{dom}(R^{\prime})\subseteq\forall
R.C^{\mathcal{I}}$, we have $x\in\forall R.C^{\mathcal{I}}$ and $\langle
x^{\prime},y\rangle\in{R}^{\mathcal{I}}$. By hypothesis, $y\in
C^{\mathcal{I}}$. $\square$

###### Lemma 8

The following properties hold.

$\displaystyle\forall R.C\sqcap\exists R.\neg C\longrightarrow\bot$ (64)
$\displaystyle C\longrightarrow D\Longrightarrow\forall
R.C\longrightarrow\forall R.D$ (65) $\displaystyle\exists R.D\sqcap\forall
R.C\longrightarrow\exists R.(D\sqcap C)$ (66)

###### Proof

  1. 1.

Arrow (64) is a consequence of (60) and (11).

  2. 2.

Due to (24), $C\longrightarrow D$ implies $\neg D\longrightarrow\neg C$. By
(53), we obtain $\exists R.\neg D\longrightarrow\exists R.\neg C$. Again, due
to (24), we have $\neg\exists R.\neg C\longrightarrow\neg\exists R.\neg D$. By
definition with (60), it follows $\forall R.C\longrightarrow\forall R.D$.

  3. 3.

To prove (66) we need category-theoretical semantics of existential and
universal restrictions. We define an object $R_{X}$ in $\mathscr{C}_{r}$ such
that $R_{X}\longrightarrow R_{(\exists R.D)}$ and
$\mathsf{dom}(R_{X})\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\leftarrow$\cr\vrule
width=0.0pt,height=2.15277pt$\hfil\scriptstyle\relbar$\cr}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\cr\vrule
width=0.0pt,height=2.15277pt$\scriptstyle\relbar$}}}\joinrel\mathrel{\raise
3.22916pt\hbox{\oalign{$\scriptstyle\relbar$\hfil\cr$\scriptstyle\vrule
width=0.0pt,height=1.50694pt\smash{\rightarrow}$\cr}}}\exists R.D\sqcap\forall
R.C$. This implies that
$\mathsf{cod}(R_{X})\longrightarrow\mathsf{cod}(R_{(\exists R.D)})$ due to the
functor $\mathsf{cod}$ from $\mathscr{C}_{r}$ to $\mathscr{C}_{c}$, and
$\mathsf{dom}(R_{X})\longrightarrow\forall R.C$. By definition, we have
$\mathsf{cod}(R_{(\exists R.D)})\longrightarrow D$. Thus,
$\mathsf{cod}(R_{X})\longrightarrow D$. Due to Arrow (61) and
$\mathsf{dom}(R_{X})\longrightarrow\forall R.C$, we obtain
$\mathsf{cod}(R_{X})\longrightarrow C$. Hence,
$\mathsf{cod}(R_{X})\longrightarrow C\sqcap D$. By the definition of
existential restrictions, we obtain $\mathsf{dom}(R_{X})\longrightarrow\exists
R.(D\sqcap C)$. $\hfill\square$

Note that both $\mathscr{C}_{c}\langle C_{0},\mathcal{O}\rangle$ and
$\mathscr{C}_{r}\langle C_{0},\mathcal{O}\rangle$ may consist of more objects.
However, new arrows should be entailed by those existing or by using the
properties given in Definitions (4-8). Adding to $\mathscr{C}_{c}\langle
C_{0},\mathcal{O}\rangle$ a new arrow that is _independent_ from those
existing leads to a semantic change of the ontology. Since all properties in
Lemma 4, 6 and 8 are consequences of those given in these definitions, they
can be used to obtain _entailed_ arrows (i.e. not independent ones).

######  Theorem 3.1 (Arrow and subsumption)

Let $C_{0}$ be an $\mathcal{ALC}$ concept and $\mathcal{O}$ an $\mathcal{ALC}$
ontology. Let $\mathscr{C}_{c}\langle C_{0},\mathcal{O}\rangle$ be an ontology
category. It holds that $\langle C_{0},\mathcal{O}\rangle\models X\sqsubseteq
Y$ (under set-theoretical semantics) if $X\longrightarrow Y$ is an arrow in
$\mathscr{C}_{c}\langle C_{0},\mathcal{O}\rangle$.

###### Proof

First, each arrow $\top\longrightarrow\neg E\sqcup F$ added to
$\mathscr{C}_{c}\langle C_{0},\mathcal{O}\rangle$ implies $E\longrightarrow F$
due to Arrows (14) and (23) for each axiom $E\sqsubseteq F$ of $\mathcal{O}$.
By set-theoretical semantics, we have $\langle C_{0},\mathcal{O}\rangle\models
E\sqsubseteq F$. Due to Lemmas 1, 2, 3, 5 and 7, for each arrow
$X\longrightarrow Y$ introduced by Definitions 4, 5, 6, 7, 8, we have $\langle
C_{0},\mathcal{O}\rangle\models X\sqsubseteq Y$.

We now introduce category-theoretical satisfiability of an $\mathcal{ALC}$
concept with respect to an $\mathcal{ALC}$ ontology.

###### Definition 9

Let $C_{0}$ be an $\mathcal{ALC}$ concept, $\mathcal{O}$ an $\mathcal{ALC}$
ontology. $C$ is category-theoretically unsatifiable with respect to
$\mathcal{O}$ if there is an ontology category $\mathscr{C}_{c}\langle
C_{0},\mathcal{O}\rangle$ which consists of the arrow
$C_{0}\longrightarrow\bot$.

Since an ontology category $\mathscr{C}_{c}\langle C_{0},\mathcal{O}\rangle$
may consist of objects arbitrarily built from the signature, Definition 9
offers possibilities to build a larger ontology category from which new arrows
can be discovered by applying arrows given in Definitions (4-8).

###### Theorem 3.2

Let $\mathcal{O}$ be an $\mathcal{ALC}$ ontology and $C$ an $\mathcal{ALC}$
concept. $C$ is category-theoretically unsatifiable with respect to
$\mathcal{O}$ iff $C$ is set-theoretically unsatifiable.

To prove this theorem, we need the following preliminary result.

###### Lemma 9

Let $\mathcal{O}$ be an $\mathcal{ALC}$ ontology and $C$ an $\mathcal{ALC}$
concept. If $C$ is set-theoretically unsatifiable with respect to
$\mathcal{O}$ then $C$ is category-theoretically unsatifiable.

In order to prove this lemma, we use a tableau algorithm to generate from a
unsatisfiable $\mathcal{ALC}$ concept with respect to an ontology a set of
completion trees each of which contains a clash ($\bot$ or a pair $\\{A,\neg
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 [8, 9] for formal details.

We use $\mathsf{sub}(C,\mathcal{O})$ to denote a set of subconcepts in NNF
(i.e. negations appear only in front of concept name) from $C$ and
$\mathcal{O}$. This set can be built by applying the following rules :(i)
$C\in\mathsf{sub}(C,\mathcal{O})$ and $\neg E\sqcup
F\in\mathsf{sub}(C,\mathcal{O})$ for each axiom $E\sqsubseteq F$; (ii) if
$\neg C\in\mathsf{sub}(C,\mathcal{O})$ then $C\in\mathsf{sub}(C,\mathcal{O})$;
(iii) if $C\sqcap D$ or $C\sqcup D\in\mathsf{sub}(C,\mathcal{O})$ then
$C,D\in\mathsf{sub}(C,\mathcal{O})$; (iv) if $\exists R.C$ or $\forall
R.C\in\mathsf{sub}(C,\mathcal{O})$ then $C\in\mathsf{sub}(C,\mathcal{O})$. A
_completion tree_ $T=\langle v_{0},V,E,L\rangle$ is a tree where $V$ is a set
of nodes, and each node $x\in V$ is labelled with
$L(x)\subseteq\mathsf{sub}(C,\mathcal{O})$, and a root $v_{0}\in V$ with $C\in
L(v_{0})$; $E$ is a set of edges, and each edge $\langle x,y\rangle\in E$ is
labelled with a role $L\langle x,y\rangle=\\{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$ : [$\sqsubseteq$-rule] for each axiom $E\sqsubseteq F$ and each node $x$,
$\neg E\sqcup F\in L(x)$; [$\sqcap$-rule] if $E\sqcap F\in L(x)$ then $E,F\in
L(x)$; [$\sqcup$-rule] if $E\sqcup F\in L(x)$ and $\\{E,F\\}\cap
L(x)=\emptyset$ then it creates two copies $T_{1}$ and $T_{2}$ of the current
tree $T$, and set $L(x_{1})\leftarrow L(x_{1})\cup\\{E\\}$,
$L(x_{2})\leftarrow L(x_{2})\cup\\{F\\}$ where $x_{i}$ in $T_{i}$ is a copy of
$x$ from $T$. [$\exists$-rule] if $\exists R.C\in L(x)$, $x$ is not blocked
and $x$ has no edge $\langle x,x^{\prime}\rangle$ with $L(\langle
x,x^{\prime}\rangle=\\{R\\}$ then it creates a successor $x^{\prime}$ of $x$,
and set $L(x^{\prime})\leftarrow\\{C\\}$, $L(\langle
x,x^{\prime}\rangle\leftarrow\\{R\\}$; [$\forall$-rule] if $\forall R.C\in
L(x)$ and $x$ has a successor $x^{\prime}$ with $L(\langle
x,x^{\prime}\rangle=\\{R\\}$ then it adds $C$ to $L(x^{\prime})$.

When [$\sqcup$-rule] is applied to a node $x$ of a completion tree $T$ with
$E\sqcup F\in L(x)$, it generates two children trees $T_{1}$ and $T_{2}$ with
a node $x_{1}$ in $T_{1}$ such that $E\sqcup F,E\in L(x_{1})$, and a node
$x_{2}$ in $T_{2}$ such that $E\sqcup F,F\in 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\sqcup F$; and $x_{1},x_{2}$ are called _disjunct_ nodes of $x$ by $E\sqcup
F$. We use $\mathbb{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
$\mathcal{O}$ then all _complete completion trees_ contain a clash (an
incomplete completion tree may contain a clash) [8, 9]. 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 [$\sqsubseteq$-rule], [$\sqcap$-rule],
[$\forall$-rule], [$\exists$-rule] and [$\sqcup$-rule] is used, and a
completion rule should be applied to the most ancestor node if applicable.
Some properties are drawn from this assumption.

  1. (P1)

If a node $x$ of a completion tree $T$ contains a clash then $x$ is a leaf
node of $T$.

  2. (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 $\mathbb{T}$.

Proof of Lemma 9. We define an ontology category $\mathscr{C}_{c}\langle
C,\mathcal{O}\rangle$ from $\mathbb{T}$ by starting from leaf trees of
$\mathbb{T}$. By (P1), each leaf tree $T$ of $\mathbb{T}$ contains a clash in
a leaf node $y$. We have $\bigsqcap_{Y\in L(y)}Y\longrightarrow\bot$. We add
an object $\bigsqcap_{Y\in L(y)}Y$ to $\mathscr{C}_{c}\langle
C,\mathcal{O}\rangle$ with the arrow. In the sequel, we try to define a
sequence of arrows started with $\bigsqcap_{Y\in L(y)}Y\longrightarrow\bot$
which makes clashes propagate from the leaves into the root of $\mathbb{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 $\mathbb{T}$.

Let $T_{1}$ and $T_{2}$ be two leaf trees of $\mathbb{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}\neq 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 $\bigsqcap_{Z\in L(z)}Z$ and add
them to $\mathscr{C}_{c}\langle C,\mathcal{O}\rangle$. Let $z^{\prime}$ be the
parent node of $y_{i}$. There is a concept $\exists R.D\in L(z^{\prime})$ and
$D\in L(y_{i})$. In addition, if $\forall R.D_{1}\in L(z^{\prime})$ and
[$\forall$-rule] is applied to $z^{\prime}$ then $D_{1}\in L(y_{i})$. We show
that $D\longrightarrow Z$ or $D_{1}\longrightarrow Z$ for each concept $Z\in
L(y_{i})$. By construction, [$\sqcup$-rule] is not applied to $y_{i}$ (and any
node from $x_{i}$ to $y_{i}$). If $Z=\neg E\sqcup F$ comes from an axiom
$E\sqsubseteq F$, then $D\longrightarrow\top\longrightarrow Z$. If $Z$ comes
from some $Z\sqcap Z^{\prime}$ then we have to have already $D\longrightarrow
Z\sqcap Z^{\prime}\longrightarrow Z$ or $D_{1}\longrightarrow Z\sqcap
Z^{\prime}\longrightarrow Z$. Hence, $\bigsqcap_{Y\in
L(y_{i})}Y\longrightarrow\bot$ implies $D\sqcap\bigsqcap_{\forall R.D_{i}\in
L(z^{\prime})}D_{i}\longrightarrow\bot$. By (52) and (66), we obtain $\exists
R.D\sqcap\bigsqcap_{\forall R.D_{i}\in L(z^{\prime})}\forall
R.D_{i}\longrightarrow\bot$, and thus $\bigsqcap_{Z\in
L(z^{\prime})}Z\longrightarrow\bot$. By using the same argument, we obtain
$\bigsqcap_{X\in L(x_{i})}X\longrightarrow\bot$. We add an object
$\bigsqcap_{X\in L(x_{i})}X$ to $\mathscr{C}_{c}\langle C,\mathcal{O}\rangle$
with the arrow.

We now show $\bigsqcap_{X\in L(x)}X\longrightarrow\bot$ where $x$ is the
disjunction node of $x_{i}$, $L(x)=W\cup\\{E\sqcup F\\}$,
$L(x_{1})=W\cup\\{E\sqcup F,E\\}$, $L(x_{2})=W\cup\\{E\sqcup F,F\\}$. Due to
(7), we have $\bigsqcap_{V\in W}V\sqcap(E\sqcup
F)\longrightarrow(\bigsqcap_{V\in W}V\sqcap E)\sqcup(\bigsqcap_{V\in W}V\sqcap
F)$. Moreover, since $\bigsqcap_{X\in L(x_{i})}X\longrightarrow\bot$, we have
$(\bigsqcap_{V\in W}V\sqcap E)\longrightarrow(\bigsqcap_{V\in
W}V\sqcap(E\sqcup F)\sqcap E\longrightarrow\bigsqcap_{X\in
L(x_{1})}X\longrightarrow\bot$ (we have $(E\sqcup F)\sqcap E\longrightarrow E$
due to (1) and (6)), and $(\bigsqcap_{V\in W}V\sqcap
F)\longrightarrow(\bigsqcap_{V\in W}V\sqcap(E\sqcup F)\sqcap
F\longrightarrow\bigsqcap_{X\in L(x_{2})}X\longrightarrow\bot$. Therefore, we
obtain $\bigsqcap_{V\in W}V\sqcap(E\sqcup F)\longrightarrow\bot$ due to (7),
then add an object $\bigsqcap_{V\in W}V\sqcap(E\sqcup F)$ to
$\mathscr{C}_{c}\langle C,\mathcal{O}\rangle$ 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 $\mathbb{T}$ to
find its parent and sibling. This process can continue and reach the root tree
$T_{0}$ of $\mathbb{T}$. We get $\bigsqcap_{X\in
L(x_{0})}X\longrightarrow\bot$ where $x_{0}$ is the root node of $T_{0}$. By
construction, we have $\\{C\\}\cup\\{\neg E\sqcup F\mid E\sqsubseteq
F\in\mathcal{O}\\}\subseteq L(x_{0})$. Let $X\in L(x_{0})$. If $X=\neg E\sqcup
F$ for some axiom $E\sqsubseteq F\in\mathcal{O}$ then
$C\longrightarrow\top\longrightarrow\neg E\sqcup F$. Moreover, if $X=E$ or
$X=F$ with $C=E\sqcap F$ then $C\longrightarrow E\sqcap F$. This implies that
$C\longrightarrow\bigsqcap_{X\in L(x_{0})}X\longrightarrow\bot$. Hence,
$C\longrightarrow\bot$. It is straightforward that $\mathscr{C}_{c}\langle
C,\mathcal{O}\rangle$ is an ontology category consisting of
$C\longrightarrow\bot$. Moreover, an arrow $\top\longrightarrow\neg E\sqcap F$
is added to $\mathscr{C}_{c}\langle C,\mathcal{O}\rangle$ for each axiom
$E\sqsubseteq F$. This completes the proof of the lemma.

Proof of Theorem 3.2. “$\Longleftarrow$”. Let $\mathscr{C}_{c}\langle
C,\mathcal{O}\rangle$ be an ontology category. Assume that there is an arrow
$C\longrightarrow\bot$ in $\mathscr{C}_{c}\langle C,\mathcal{O}\rangle$. Every
arrow $X\longrightarrow Y$ added to $\mathscr{C}_{c}\langle
C,\mathcal{O}\rangle$ must be one of following cases: (i) $X\sqsubseteq Y$ is
an axiom of $\mathcal{O}$. Thus, $\mathcal{O}\models X\sqsubseteq Y$. (ii)
$X\longrightarrow Y$ is added by Definitions 4, 5, 6, 7, 8. Due to Lemma
LABEL:lem:arrow-entail, we have $\mathcal{O}\models X\sqsubseteq Y$. (iii)
$X\longrightarrow Y$ is obtained by transitivity from $X\longrightarrow Z$ and
$Z\longrightarrow Y$. It holds that $\mathcal{O}\models X\sqsubseteq Z$ and
$\mathcal{O}\models Z\sqsubseteq Y$ imply $\mathcal{O}\models X\sqsubseteq Y$.
Hence, if $\mathscr{C}_{c}\langle C,\mathcal{O}\rangle$ consists of an arrow
$C\longrightarrow\bot$, then $\mathcal{O}\models C\sqsubseteq\bot$.

“$\Longrightarrow$”. A consequence of Lemma 9. $\square$

##  4 Conclusion and Future Work

We have presented a rewriting of the usual set-theoretical semantics of
$\mathcal{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 separate
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_.

## 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] S. Mac Lane, I. Moerdijk, Sheaves in Geometry and Logic, Springer, 1992.
  * [8] 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, Springer-Verlag, St Andrews, Scotland, UK, 2000, p. 118.
  * [9] I. Horrocks, U. Sattler, A tableau decision procedure for $\mathcal{SHOIQ}$, Journal Of Automated Reasoning 39 (3) (2007) 249–276.