Reasoning in the Description Logic ALC under Category Semantics
share
We present in this paper a reformulation of the usual set-theoretical semantics of the description logic 𝒜ℒ𝒞 with general TBoxes by using categorical language. In this setting, 𝒜ℒ𝒞 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 𝒜ℒ𝒞. This feature allows us to define a sublogic of 𝒜ℒ𝒞 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 PSPACE by proposing a deterministic algorithm for checking concept satisfiability which runs in polynomial space.
READ FULL TEXT