Languages based on Description Logics (DLs) [1] such as OWL [2], OWL2 [3], are widely used to represent ontologies in semantics-based applications. ℒ is the smallest DL involving roles which is closed under negation. It is a suitable logic for a first attempt to replace the usual set-theoretical semantics by another one. 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. It is well known that ℒ with general TBoxes is EXPTIME-complete [4, 5] while ℒ without TBox is PSPACE-complete [6]. Hence, the interaction between existential and universal restrictions with general TBoxes would be responsible for an intractable space complexity if PSPACE⊊ EXPTIME. The main motivation of this work consists in identifying a sublogic of ℒ with general TBoxes which allows to reduce the reasoning complexity without losing too much of the expressive power. To reduce space complexity when reasoning with ℒ under the usual set-theoretical semantics, one can restrict expressiveness of TBoxes by preventing them from having cyclic axioms [7]. This restriction may be too strong for those who wish to express simple knowledge of cyclic nature such as Human ⊑ ∃hasParent.Human. However, we can find a sublogic of ℒ under category-theoretical semantics such that it allows to fully express general TBoxes and only needs to drop a part of the semantics of universal restrictions. Such a sublogic is undefinable in the usual set-theorectical semantics. Indeed, a
1. Introduction universal restriction ∀. in ℒ can be defined under category-theoretical semantics by using the following two informal properties (that will be developed in more detail below, in Definition 3): (i) ∀. is “very close” to ¬∃.¬; and (ii) ∃. ⊓ ∀. is “very close” to ∃.( ⊓ ). We can observe that Property (ii) is a (weak) representation of the interaction between universal and existential restrictions. If we may just remove this interaction from the categorical semantics of universal restriction, we obtain a new logic, namely ℒ∀, in which reasoning will be tractable in space. The semantic loss caused by this removal might be tolerable in certain cases. We illustrate it with the example below.
Example 1. Consider for instance the following ℒ TBox:
HappyChild ⊑ ∃eatsFood.Dessert ⊓ ∀eatsFood.HotMeal
Dessert ⊑ ¬HotMeal
As in the usual set-theoretical semantics, nobody can be a HappyChild under category-theoretical
semantics: the concept is unsatisfiable in this world. Indeed, according to the first axiom if somebody
is a HappyChild, then they must simultaneously (
Under the category-theoretical semantics that we will define in this paper ( ℒ∀), the first axiom alone does not allow to entail that if somebody is a HappyChild then they eat HotMeal. This is due to the fact that the element of the definition of universal quantification that was there to represent Property (ii) has been dropped, and that unlike set-theoretical semantics, we no longer have a set of individuals providing an extensional “support” for the second subconcept. 2. Category-Theoretical Semantics of ℒ We can observe that the set-theoretical semantics of ℒ is based on set membership relationships, while ontology inferences, such as consistency or concept subsumption, involve set inclusions. This explains why inference algorithms developed in this setting often have to build sets of individuals connected in some way for representing a model. In this section, we use some basic notions in category theory to characterize the semantics of ℒ. Instead of set membership, in this categorical language, we use “objects” and “arrows” to define semantics of a given object.
Definition 1 (Syntax categories). Let R and C be non-empty sets of role names and concept names respectively. We define a concept syntax category C and a role syntax category C from the signature ⟨C, R⟩ as follows: 1. Each role name in R is an object of C. In particular, there are initial and terminal objects ⊥ and ⊤ in C with arrows →− ⊤ and ⊥ →− for all object of C.
There is also an identity arrow →− for each object of C. 3. If there are arrows →− in C (resp. C).
and →− in C (resp. C), then there is an arrow →− 4. There are two functors dom and cod from C to C, i.e. they associate two objects dom() and cod() of C to each object of C such that a) dom(⊤) = ⊤, cod(⊤) = ⊤, dom(⊥) = ⊥ and cod(⊥) = ⊥.
′ in C then there are arrows dom() →− dom(′) and b) if there is an arrow →−
cod() →− cod(′). c) if there are arrows →−
dom(′′) and cod() →− d) if there is an arrow dom() →− ⊥ →− ⊥ in C.
′ →− cod(′′).
′′ in C then there are arrows dom() →− or cod() →− ⊥ in C, then there is an arrow For each arrow →− in C or C, and are respectively called domain and codomain of the arrow. We use also Ob(C ) and Hom(C ) to denote the collections of objects and arrows of a category C .
Definition 1 provides a general framework with syntax elements and necessary properties from category theory. We need to “instantiate" it to obtain categories which capture semantic constraints coming from axioms.
Definition 2 (Ontology categories). Let be an ℒ concept and an ℒ ontology from a signature ⟨C, R⟩. We define a concept ontology category C⟨, ⟩ and a role ontology category C⟨, ⟩ as follows: 1. C⟨, ⟩ and C⟨, ⟩ are syntax categories from ⟨C, R⟩. 2. is an object of C⟨, ⟩. 3. If ⊑ is an axiom of , then , are objects and →− is an arrow of C⟨, ⟩.
In the sequel, we introduce category-theoretical semantics of disjunction, conjunction, negation, existential and universal restriction objects if they appear in C⟨, ⟩. Some of them require more explicit properties than those needed for the set-theoretical semantics. Definition 3 (Category-theoretical semantics). Assume that C⟨, ⟩ and C⟨, ⟩ have all concept and role objects used in the following properties. Category-theoretical semantics of disjunction, conjunction, negation, existential and univeral restrictions are defined by using arrows in C⟨, ⟩ as follows. Conjunction: Negation: →− ⊔ and →− For all object of C⟨, ⟩, →− ⊔ are arrows of C⟨, ⟩ and →− imply ⊔ →− ⊓ →− and ⊓ →− For all object of C⟨, ⟩, →− ⊓ ( ⊔ ) →− ( ⊓ ) ⊔ ( ⊓ ) is an arrow of C⟨, ⟩ are arrows of C⟨, ⟩ and →− imply →− ⊓ ⊓ ¬ →− ⊥ and ⊤ →− ⊔ ¬ are arrows of C⟨, ⟩ For all object of C⟨, ⟩, ⊓ →− ⊥ implies →− ¬ For all object of C⟨, ⟩, ⊤ →− ⊔ implies ¬ →− Existential restriction: (∃.) →− , cod((∃.)) →−
are arrows of C⟨, ⟩ dom((∃.)) ← − −− −→ ∃. are arrows of C⟨, ⟩ For all object ′ of C⟨, ⟩, ′ →− , cod(′) →− imply dom(′) →− Universal restriction: ∀. ← − −− −→ ¬∃.¬ are arrows of C⟨, ⟩ For all object ′ of C⟨, ⟩, ′ →− , dom(′) →− ∀ . imply cod(′) →−
Note that both C⟨, ⟩ and C⟨, ⟩ may consist of more objects. However, new arrows
should be derived from those existing or the properties given in Definitions (
Theorem 1. Let be an ℒ ontology and 0 an ℒ concept. 0 is category-theoretically
unsatifiable with respect to if 0 is set-theoretically unsatifiable.
(
To show the independence of Property (13) under the category semantics, we can build a
category that verifies Properties (
To check satisfiability of an ℒ∀ concept 0 with respect to an ontology , we define a set of saturation rules each of which represents a property introduced for the category semantics except for Property (5) (distributivity). We initialize an ontology category C ⟨0, ⟩ and saturate it by applying the saturation rules to C⟨0, ⟩ until no rule is applicable.
Theorem 2. Satisfiability of an ℒ∀ concept with respect to an ontology can be decided in polynomial space.
As mentioned above, we do not introduce a saturation rule to directly capture Property (5) since this may lead to adding an exponential number of objects. The polynomial complexity in space results from constructing a category C by using a rule, namely [⊔dis-rule], that call an algorithm check instead of applying directly Property (5). This algorithm traverses at most all binary trees where is an object of the form = (1 ⊔ 1) ⊓ · · · ⊓ ( ⊔ ) that must be included in C. Such a tree is composed of nodes of the form 1 ⊓ · · · ⊓ where ∈ {, , ⊔ } for 1 ≤ ≤ . Such nodes 1 ⊓ · · · ⊓ are not necessarily included in C but each conjunct is an object of C. This allows the algorithm check to discover all arrows →− where , are objects of C by using arrows of C and those resulting from distributivity (Property (5)) applied to nodes of trees . Since the nodes of a tree can be encoded as binary numbers between 0 and 2 − 1, we can use an algorithm that runs in polynomial space to traverse all its nodes. [4] K. Schild, A correspondence theory for terminological logics: preliminary report, in: Proceedings of the 12th international joint conference on Artificial intelligence, 1991, p. 466–471. [5] F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge
University Press, 2017. [6] M. Schmidt-Schauß , G. Smolka, Attributive concept descriptions with complements,
Artificial Intelligence 48 (1991) 1–26. [7] F. Baader, J. Hladik, R. Peñaloza, Automata can show PSpace results for description logics, Information and Computation 206 (2008) 1045–1056. Special Issue: 1st International Conference on Language and Automata Theory and Applications (LATA 2007).