Reasoning in the Description Logic ALC under Category Semantics

TL;DR

This paper reformulates the description logic ALC using category theory, enabling modular semantics and defining a PSPACE sublogic with an efficient satisfiability algorithm.

Contribution

It introduces a categorical semantics for ALC, defines a new sublogic with reduced complexity, and provides a polynomial space algorithm for concept satisfiability.

Findings

Categorical semantics offers a modular view of ALC.

A new sublogic of ALC is defined with lower complexity.

A polynomial space algorithm for satisfiability is proposed.

Abstract

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.