Soutenance de thèse Ludovic Brieulle

Une des problématiques liées aux logiques de description est de trouver un équilibre entre l’expressivité de celles-ci et la complexité de leurs raisonnements : avec peu d’expressivité, les résultats obtenus peuvent être peu intéressants ou pertinents. Au contraire, une complexité trop élevée peut poser des problèmes de temps d’exécution ou d’aboutissement pour une large quantité de donnée, il s’agit du problème de passage à l’échelle, par exemple Snomed possède plus de 600000 concepts et plus d’un million d’axiomes. Les logiques utilisées pour les ontologies médicales sont tractables, mais ne permettent pas d’exprimer la négation. Or il peut être tout à fait envisageable de vouloir exprimer des connaissances négatives médicales. Cependant, ajouter la négation à ces logiques provoque une explosion de la complexité rendant ces logiques intractables et donc leur faisant perdre leur avantage.

Puisque les raisons pour lesquelles la complexité augmente sont intrinsèquement lié à la théorie des ensembles, nous proposons alors d’utiliser la théorie des catégories pour définir une nouvelle sémantique dite catégorielle. Les ensembles sont remplacés par des objets d’une catégorie et l’inclusion ensembliste par les flèches de cette même catégorie. Nous utilisons alors des structures de la théorie des catégories pour définir la sémantique de différents constructeurs tout en s’assurant de la compatibilité des définitions avec celles de la sémantique ensembliste. En exploitant la modularité des définitions de cette sémantique catégorielle par rapport à la sémantique ensembliste, nous pouvons enlever des propriétés dites indépendantes que nous jugeons responsables de la complexité élevée des raisonnements. Nous obtenons ainsi des langages exprimables uniquement en sémantique catégorielle avec soit moins d’expressivité pour une complexité réduite, soit un gain d’expressivité limité pour une complexité similaire.

Le procédé consiste à commencer par établir une équivalence sémantique d’une logique en sémantique ensembliste et en sémantique catégorielle. Puis, nous enlevons une partie de la définition d’un ou plusieurs constructeurs afin d’obtenir de nouvelles logiques de description exprimables uniquement en sémantique catégoriel et nous raisonnons ensuite sur ces nouvelles logiques. Dans un premier cas, nous partons de la logique ALC pour obtenir une nouvelle logique ALC affaiblie en utilisant une restriction universelle affaiblie, mais pour laquelle le raisonnement est NP-complet contre une complexité ExpTime-complète pour ALC.  Nous avons également implémenté un nouveau raisonneur Arrows qui permet de décider de la satisfiabilité d’un concept en ALC affaiblie. Pour le deuxième cas, nous partons cette fois-ci de SH pour obtenir une extension de EL admettant une version affaiblie de la négation, en enlevant certaines des propriétés indépendantes de la disjonction et de la restriction universelle. Ceci en conservant la tractabilité des logiques de la famille EL.

One of the main problematic of description logics is to find a balance between expressivity and the complexity of reasoning on these logics. Indeed, not enough expressivity and the knowledge that can be extracted isn’t much relevant or of any help. On the other side, if it is too much expressive, there is a risk that, for example when there is too much data, that reasoning takes up too much time or even does not return anything if there are not enough resources. This is called the scaling problem. For example, Snomed has around 600000 concepts and more than one million axioms. DLs used to reason on such ontologies are tractable and one might want to express negative knowledge in medical context. However, adding negation makes these logics lose their tractability and main advantage.

Since the reasons for the increase in complexity are intrinsically linked to set theory, we propose to use category theory to develop brand new categorical semantics. Instead of sets, concepts will be associated with objects and arrows will replace set inclusions. Using definition and construction from category theory, we define the semantic of various logical constructors and ensure that their categorical properties are compatible with set semantics. By making use of the modularity of category semantics definitions compared to set semantics, we remove independent properties that we judge responsible for the rise in complexity for reasoning in some DLs. By doing this, we obtain completely new logics that are expressible only in categorical semantics.

The way we proceed is by first establishing the semantic equivalence of set semantics and categorical semantics for a given DL, and then we « weaken » some constructor to remove the interactions that we deem problematic. From there, we obtain a new logic that makes sense only in category semantics since those interactions are mathematical consequences of the definition in set semantics, and reason on those new logics. The first one is derived from ALC, by weakening the universal restriction we obtain a new logic we call weakened ALC for which reasoning is NP-complete compared to ALC for which reasoning is ExpTime-complete. We also implemented a reasoner Arrows that determines the satisfiability of a concept in weakened ALC. The other logics we developed is derived from the logic SH. By weakening the universal restriction and the disjunction, we define an extension of EL that allows for a weakened version of the negation while keeping the tractability of EL family members.