Category-theoretical Semantics of the Description Logic ALC (extended version)

TL;DR

This paper introduces a category-theoretical framework for the semantics of the description logic ALC, offering a modular and potentially more flexible approach to reasoning in description logics.

Contribution

It reformulates ALC semantics using category theory, replacing set membership with categorical objects and arrows, enabling new reasoning algorithm designs.

Findings

Provides a categorical semantics for ALC

Enhances modularity of description logic interpretation

Suggests new directions for reasoning algorithms

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, 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.