=Paper=
{{Paper
|id=Vol-3263/abstract-7
|storemode=property
|title=Reasoning in the Description Logic ALC under Category Semantics (Extended Abstract)
|pdfUrl=https://ceur-ws.org/Vol-3263/abstract-7.pdf
|volume=Vol-3263
|authors=Ludovic Brieulle,Chan Le Duc,Pascal Vaillant
|dblpUrl=https://dblp.org/rec/conf/dlog/BrieulleDV22
}}
==Reasoning in the Description Logic ALC under Category Semantics (Extended Abstract)==
<pdf width="1500px">https://ceur-ws.org/Vol-3263/abstract-7.pdf</pdf>
<pre>
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).

</pre>