Vincent est chercheur postdoctoral à l’Université de Bordeaux.
Titre : Implication de requêtes pour S, revisitée.
Résumé : En logique de description, le problème d’implication de requêtes se formule ainsi : étant donnés une ABox A (c’est-à-dire une structure finie), une ontologie T (ou TBox, un ensemble fini de contraintes) et une requête q, toute complétion de A satisfaisant T vérifie-t-elle nécessairement aussi q ?
Nous étudions ce problème dans le cadre de S, extension d’ALC (= logique modale) dans laquelle certains rôles — c’est-à-dire des relations binaires — peuvent être déclarés transitifs. On savait déjà que ce problème est coNExpTime-difficile [Thomas Eiter et al., 2009] et dans 2ExpTime [Diego Calvanese et al., 1998].
Dans ce séminaire sera présenté un article récent, publié à AAAI, dans lequel nous comblons cet écart et établissons la complexité exacte du problème. Nous y démontrons notamment la dichotomie suivante : le problème est 2ExpTime-complet en présence d’au moins deux rôles transitifs, mais devient coNExpTime-complet lorsque l’instance n’en contient qu’un seul (et un nombre arbitraire de rôles non transitifs). Nous nous concentrerons en particulier sur ce cas plus simple, dont la résolution repose sur une utilisation élégante d’une variante d’automates sur arbres infinis.
Site web : https://vimichielini.com/