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 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-theore\-tical semantics provides a more modular representation of the semantics of $\mathcal{ALC}$ and a new way to design algorithms for reasoning.
翻译：分类理论可以用于在第一个正序逻辑中说明公式而不使用设定成员。 逻辑中的若干显著结果, 如连续假设的证据可以在分类理论中进行优雅的重写。 我们在本文件中建议通过使用绝对语言重拟描述逻辑 ALC 的通常设定理论语义。 在此背景下, $\ mathcal{ ALC}} 概念被表述为对象、 以箭头形式进行概念子假定, 以及以成员身份作为对象和类别箭头的逻辑量化符。 这样的分类- 理论语义提供了更模块化的 $\ mathcal{ ALC} 的语义表达方式, 以及设计推理算法的新方法 。
相关内容
微信扫码咨询专知VIP会员