论文标题
描述中的推理逻辑ALC类别语义下
Reasoning in the Description Logic ALC under Category Semantics
论文作者
论文摘要
我们在本文中介绍了描述逻辑$ \ mathcal {alc} $的常规设置理论语义的重新制定，并使用一般的tbox使用分类语言进行了重新制定。在这种情况下，$ \ MATHCAL {ALC} $概念被表示为对象，概念归因为箭头，而成员资格是类别的对象和箭头的逻辑量词。这样的基于类别的语义提供了$ \ Mathcal {Alc} $语义的更模块化表示。此功能使我们能够通过删除存在性和通用限制之间的相互作用来定义$ \ Mathcal {Alc} $的子量表，这将使空间中的指数复杂性负责。在通常的集合理论语义中，这种sublogic是无法定义的，我们表明，这种sublogic是{\ sc {pspace}}，通过提出一种确定性算法来检查在多项式空间中运行的概念可满足性的确定性算法。
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.
