We present in this paper a reformulation of the usual set-theoretical
semantics of the description logic $\mathcal{ALC}$ with general TBoxes 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-based
semantics provides a more modular representation of the semantics of
$\mathcal{ALC}$. This feature allows us to define a sublogic of $\mathcal{ALC}$
by dropping the interaction between existential and universal restrictions,
which would be responsible for an exponential complexity in space. Such a
sublogic is undefinable in the usual set-theoretical semantics, We show that
this sublogic is {\sc{PSPACE}} by proposing a deterministic algorithm for
checking concept satisfiability which runs in polynomial space.

本文通过使用范畴语言重新表达了具有一般 TBox 的描述逻辑 ALC 通常的集合论语义，从而为 ALC 的语义提供了一种更模块化的表示。我们展示了一个多项式空间的确定性算法用于检查概念满足性的子逻辑，该子逻辑在传统的集合论语义中是无法定义的。