Reasoning in the Description Logic ALC under Category Semantics Extended Abstract Ludovic Brieulle1 , Chan Le Duc1 and Pascal Vaillant1 1 UniversitΓ© Sorbonne Paris Nord, LIMICS, INSERM, U1142, F-93000, Bobigny, France 1. Introduction 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 DL 2022: 35th International Workshop on Description Logics, August 7–10, 2022, Haifa, Israel $ ludovic.brieulle@univ-paris13.fr (L. Brieulle); chan.leduc@univ-paris13.fr (C. Le Duc); pascal.vaillant@univ-paris13.fr (P. Vaillant) Β© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) 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 (1) have some Dessert to eat, and (2) eat only HotMeal, which contradicts the second axiom. Now, if the second axiom is removed from the TBox, under set-theoretical semantics, the first axiom entails that if somebody is a HappyChild, then they eat HotMeal. In fact, the first subconcept (βˆƒeatsFood.Dessert) ensures that there exists at least one food item that they eat, and the second one (βˆ€eatsFood.HotMeal) that this food is necessarily HotMeal. 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 rela- tionships, 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π‘Ÿ . 2. Each concept name in C is an object of C𝑐 . In particular, βŠ₯ and ⊀ are respectively initial and terminal objects, i.e. there are arrows 𝐢 βˆ’β†’ ⊀ and βŠ₯ βˆ’β†’ 𝐢 for each object 𝐢 of C𝑐 . Furthermore, for each object 𝐢 of C𝑐 there is an identity arrow 𝐢 βˆ’β†’ 𝐢, for each object 𝑅 of Cπ‘Ÿ there are two objects of C𝑐 , namely dom(𝑅) and cod(𝑅), and for each object βˆƒπ‘….𝐢 of C𝑐 there is an object 𝑅(βˆƒπ‘….𝐢) of Cπ‘Ÿ . 3. If there are arrows 𝐸 βˆ’β†’ 𝐹 and 𝐹 βˆ’β†’ 𝐺 in C𝑐 (resp. Cπ‘Ÿ ), then there is an arrow 𝐸 βˆ’β†’ 𝐺 in C𝑐 (resp. Cπ‘Ÿ ). 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(𝑅βŠ₯ ) = βŠ₯. b) if there is an arrow 𝑅 βˆ’β†’ 𝑅′ in Cπ‘Ÿ then there are arrows dom(𝑅) βˆ’β†’ dom(𝑅′ ) and cod(𝑅) βˆ’β†’ cod(𝑅′ ). c) if there are arrows 𝑅 βˆ’β†’ 𝑅′ βˆ’β†’ 𝑅′′ in Cπ‘Ÿ then there are arrows dom(𝑅) βˆ’β†’ dom(𝑅′′ ) and cod(𝑅) βˆ’β†’ cod(𝑅′′ ). d) if there is an arrow dom(𝑅) βˆ’β†’ βŠ₯ or cod(𝑅) βˆ’β†’ βŠ₯ in C𝑐 , then there is an arrow 𝑅 βˆ’β†’ 𝑅βŠ₯ in Cπ‘Ÿ . 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, nega- tion, 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. Disjunction: 𝐢 βˆ’β†’ 𝐢 βŠ” 𝐷 and 𝐷 βˆ’β†’ 𝐢 βŠ” 𝐷 are arrows of C𝑐 ⟨𝐢, π’ͺ⟩ (1) For all object 𝑋 of C𝑐 ⟨𝐢, π’ͺ⟩, 𝐢 βˆ’β†’ 𝑋 and 𝐷 βˆ’β†’ 𝑋 imply 𝐢 βŠ” 𝐷 βˆ’β†’ 𝑋 (2) Conjunction: 𝐢 βŠ“ 𝐷 βˆ’β†’ 𝐢 and 𝐢 βŠ“ 𝐷 βˆ’β†’ 𝐷 are arrows of C𝑐 ⟨𝐢, π’ͺ⟩ (3) For all object 𝑋 of C𝑐 ⟨𝐢, π’ͺ⟩, 𝑋 βˆ’β†’ 𝐢 and 𝑋 βˆ’β†’ 𝐷 imply 𝑋 βˆ’β†’ 𝐢 βŠ“ 𝐷 (4) 𝐢 βŠ“ (𝐷 βŠ” 𝐸) βˆ’β†’ (𝐢 βŠ“ 𝐷) βŠ” (𝐢 βŠ“ 𝐸) is an arrow of C𝑐 ⟨𝐢, π’ͺ⟩ (5) Negation: 𝐢 βŠ“ ¬𝐢 βˆ’β†’ βŠ₯ and ⊀ βˆ’β†’ 𝐢 βŠ” ¬𝐢 are arrows of C𝑐 ⟨𝐢, π’ͺ⟩ (6) For all object 𝑋 of C𝑐 ⟨𝐢, π’ͺ⟩, 𝐢 βŠ“ 𝑋 βˆ’β†’ βŠ₯ implies 𝑋 βˆ’β†’ ¬𝐢 (7) For all object 𝑋 of C𝑐 ⟨𝐢, π’ͺ⟩, ⊀ βˆ’β†’ 𝐢 βŠ” 𝑋 implies ¬𝐢 βˆ’β†’ 𝑋 (8) Existential restriction: 𝑅(βˆƒπ‘….𝐢) βˆ’β†’ 𝑅, cod(𝑅(βˆƒπ‘….𝐢) ) βˆ’β†’ 𝐢 are arrows of C𝑐 ⟨𝐢, π’ͺ⟩ (9) dom(𝑅(βˆƒπ‘….𝐢) ) ← βˆ’βˆ’β†’ βˆƒπ‘….𝐢 are arrows of C𝑐 ⟨𝐢, π’ͺ⟩ βˆ’βˆ’ (10) For all object 𝑅′ of Cπ‘Ÿ ⟨𝐢, π’ͺ⟩, 𝑅′ βˆ’β†’ 𝑅, cod(𝑅′ ) βˆ’β†’ 𝐢 imply dom(𝑅′ ) βˆ’β†’ dom(𝑅(βˆƒπ‘….𝐢) ) (11) Universal restriction: βˆ€π‘….𝐢 ← βˆ’βˆ’β†’ Β¬βˆƒπ‘….¬𝐢 are arrows of C𝑐 ⟨𝐢, π’ͺ⟩ βˆ’βˆ’ (12) β€² β€² β€² β€² For all object 𝑅 of Cπ‘Ÿ ⟨𝐢, π’ͺ⟩, 𝑅 βˆ’β†’ 𝑅, dom(𝑅 ) βˆ’β†’ βˆ€π‘….𝐢 imply cod(𝑅 ) βˆ’β†’ 𝐢 (13) 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 (1-3). Adding to C𝑐 ⟨𝐢, π’ͺ⟩ a new arrow that is independent from those existing leads to a semantic change of the ontology. We now introduce category-theoretical satisfiability of an π’œβ„’π’ž concept with respect to an π’œβ„’π’ž ontology. Definition 4. Let 𝐢0 be an π’œβ„’π’ž concept, π’ͺ an π’œβ„’π’ž ontology. 𝐢 is category-theoretically unsatifiable with respect to π’ͺ if there is an ontology category C𝑐 ⟨𝐢0 , π’ͺ⟩ which has an arrow 𝐢0 βˆ’β†’ βŠ₯. Theorem 1. Let π’ͺ be an π’œβ„’π’ž ontology and 𝐢0 an π’œβ„’π’ž concept. 𝐢0 is category-theoretically unsatifiable with respect to π’ͺ iff 𝐢0 is set-theoretically unsatifiable. 3. Reasoning in a Sublogic of π’œβ„’π’ž In this section, we identify a new sublogic of π’œβ„’π’ž, namely π’œβ„’π’ž βˆ€ , obtained from π’œβ„’π’ž with all the properties introduced in Definition 3, except for Property (13). This sublogic cannot be defined under the usual set-theoretical semantics since Property (13) is not independent from the properties defined for existential restriction and Property (12) in this setting. Indeed, for every interpretation ℐ it holds that if 𝑅′ ℐ βŠ† 𝑅ℐ , dom(𝑅′ )ℐ βŠ† βˆ€π‘….𝐢 ℐ and π‘₯ ∈ cod(𝑅′ )ℐ , then π‘₯ ∈ 𝐢ℐ . To show the independence of Property (13) under the category semantics, we can build a category that verifies Properties (1-12) but Property (13) cannot be derived from this category. Definition 5 (Category-theoretical unsatisfiability in π’œβ„’π’ž βˆ€ ). Let 𝐢 be an π’œβ„’π’ž βˆ€ concept, π’ͺ an π’œβ„’π’ž βˆ€ ontology. 𝐢 is category-theoretically unsatifiable with respect to π’ͺ if there is an ontology category C𝑐 ⟨𝐢, π’ͺ⟩ which has an arrow 𝐢 βˆ’β†’ βŠ₯. 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. References [1] F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, P. F. Patel-Schneider (Eds.), The Description Logic Handbook: Theory, Implementation and Applications, Second Edition, Cambridge University Press, 2010. [2] P. Patel-Schneider, P. Hayes, I. Horrocks, Owl web ontology language semantics and abstract syntax, in: W3C Recommendation, 2004. [3] B. Cuenca Grau, I. Horrocks, B. Motik, B. Parsia, P. Patel-Schneider, U. Sattler, Owl 2: The next step for owl, journal of web semantics: Science, services and agents, World Wide Web 6 (2008) 309–322. [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 log- ics, Information and Computation 206 (2008) 1045–1056. Special Issue: 1st International Conference on Language and Automata Theory and Applications (LATA 2007).