Reasoning in the Description Logic ALC under Category Semantics

We present in this paper a reformulation of the usual set-theoretical semantics of the description logic ALC with general TBoxes 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-based semantics provides a more modular representation of the semantics of ALC. This feature allows us to define a sublogic of 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 scPSPACE by proposing a deterministic algorithm for checking concept satisfiability which runs in polynomial space.