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.
翻译:在本文中, 我们通过使用绝对语言对描述逻辑 $\ mathcal{ ALC} $ 和普通 TBoxs 的通常设置的理论语义进行重拟。 在这种背景下, $\ mathcal{ ALC} $ 的概念被表述为对象、 概念子假设作为箭头, 以及成员作为对象和类别箭头的逻辑量化符。 这种基于分类的语义提供了更模块化的 $\ mathcal{ ALC} $ 的语义表达。 这个功能使我们能够通过放弃存在和普遍限制之间的相互作用来定义一个 $\ mathcal{ ALC} 的子logic 。 这对于空间中的指数复杂性是不可定义的。 在常规设置的理论语义中, 我们通过提出用于检查多位空间中的概念是否具有相对性的概念的确定性算法, 表明这个子语义是 { PSPACE ⁇ 。