Partially Finite Model Reasoning in Description Logics Extended Version

1. Énoncé du problème

L'article comble le fossé entre le raisonnement sur les modèles infinis (standard en Logiques de Description, où les modèles peuvent être arbitrairement grands) et le raisonnement sur les modèles finis (standard dans les bases de données, où les domaines sont finis). Bien que de nombreuses Logiques de Description (LD) présentent une contrôlabilité finie (où l'inférence de requêtes est identique pour les modèles finis et infinis), d'autres, telles que $\mathcal{S}$ (une extension de $\mathcal{ALC}$ avec des rôles transitifs), ne le font pas. Dans ces logiques, une requête peut être entaillée dans tous les modèles finis mais pas dans les modèles infinis, ou inversement.

Les auteurs introduisent le Raisonnement sur les Modèles Partiellement Finis. Dans ce mode hybride :

• Une Base de Connaissances (BC) est fournie avec un concept distingué $F$.
• La tâche de raisonnement ne considère que les modèles où l'interprétation de $F$ est un ensemble fini d'individus.
• Le reste du modèle (les éléments n'appartenant pas à $F$) peut être infini.
• Objectif : Décider si une Requête Conjonctive (RC) $Q$ est entaillée par la BC sous la contrainte que $F$ est fini (noté $K \models_F Q$).

Ce cadre généralise à la fois l'entailement standard (où aucun concept n'est restreint) et l'entailement fini (où le domaine entier est restreint). Il sert également de fondement théorique pour l'inclusion de requêtes avec prédicats fermés, où certains prédicats sont supposés avoir des extensions finies.

2. Méthodologie

Les auteurs développent une technique de preuve sophistiquée pour décider l'entailement partiellement fini pour la logique $\mathcal{S}$. La méthodologie implique plusieurs étapes clés :

A. Quasi-déroulement

Pour gérer les modèles infinis tout en maintenant la partie « finie » ($F$) gérable, les auteurs introduisent le quasi-déroulement.

• Contrairement au déroulement standard (qui crée un arbre en dupliquant chaque nœud), le quasi-déroulement crée une structure arborescente où les éléments critiques (ceux appartenant à $F$) ne sont pas dupliqués.
• Seuls les éléments non critiques sont dupliqués le long des chemins. Cela garantit que la structure résultante possède un ensemble fini de nœuds critiques, préservant la propriété « partiellement finie » tout en permettant au reste du modèle d'être arborescent pour une analyse plus facile.

B. Interprétations élémentaires

Les auteurs définissent une classe de structures finies appelées interprétations élémentaires pour servir de représentations finies de contre-modèles potentiels. Elles sont construites de manière hiérarchique :

1. Singletons/Cycles/Clusters critiques : Briques de base.
2. Arbres de boucles : Arbres formés en attachant des arbres de boucles à des singletons ou des cycles (similaires à des cactus).
3. Interprétations élémentaires : Arbres construits en attachant des arbres de boucles et des clusters critiques.
   L'idée centrale est que tout contre-modèle peut être transformé en une interprétation élémentaire via un quasi-déroulement sans perdre la propriété d'être un contre-modèle.

C. Blocage coloré et quotients

Pour gérer plusieurs rôles transitifs et assurer l'existence d'un contre-modèle fini avec les propriétés requises, l'article adapte le Théorème du blocage coloré.

• Ils définissent un coloriage $k$-épars des éléments critiques.
• En utilisant une relation d'équivalence basée sur les $k$-voisinages, ils construisent une interprétation quotient.
• Ils prouvent que si une requête n'est pas satisfaite dans le modèle infini original, elle n'est pas non plus satisfaite dans le quotient (qui est partiellement fini), à condition que le coloriage soit suffisamment éparse.

D. Le « gonflement » et la décidabilité

Pour rendre le problème décidable, les auteurs remplacent la condition « le quasi-déroulement ne satisfait pas $Q$ » par une condition vérifiable sur une version gonflée de l'interprétation élémentaire ($G_n$).

• Ils « gonflent » les cycles dans l'interprétation élémentaire jusqu'à une longueur de $2n+1$ (où $n$ est le nombre de variables dans la requête).
• Ils prouvent que vérifier si la structure gonflée $G_n$ satisfait la requête est équivalent à vérifier le quasi-déroulement pour des requêtes de taille $n$.
• Cela permet d'utiliser une procédure d'élimination de types (similaire aux approches basées sur les automates) pour rechercher un témoin (un contre-modèle) dans un espace de recherche doublement exponentiel.

3. Contributions clés

1. Formalisation du raisonnement partiellement fini : L'article initie l'étude systématique du raisonnement où seules des parties spécifiques d'un modèle sont contraintes d'être finies.
2. Résultat de complexité pour $\mathcal{S}$ : Les auteurs prouvent que l'entailement de requêtes partiellement fini pour $\mathcal{S}$ est 2-ExpTime-complet.
   • Cela correspond à la complexité de l'entailement infini standard et de l'entailement fini pour $\mathcal{S}$, montrant que le mode hybride n'augmente pas la complexité computationnelle.
3. Nouvelles techniques de preuve : La solution implique une « chirurgie de modèle infini », combinant quasi-déroulement, interprétations élémentaires et blocage coloré d'une manière qui va au-delà de la simple combinaison d'arguments pour les cas fini et infini.
4. Application aux prédicats fermés : L'article démontre que l'inclusion de requêtes en présence de prédicats fermés peut être réduite à l'entailement partiellement fini. Cela fournit une nouvelle borne supérieure de complexité pour le problème des prédicats fermés dans les LD expressives.

4. Résultats

• Théorème principal (Théorème 16) : L'entailement partiellement fini des requêtes conjonctives pour la logique $\mathcal{S}$ est 2-ExpTime-complet.
• Caractérisation du témoin : Si une BC n'entaile pas partiellement et finiment une requête, il existe une interprétation « élémentaire par morceaux » de taille bornée (exponentielle par rapport à la taille de la BC) dont le quasi-déroulement sert de contre-modèle.
• Réduction : L'inclusion de requêtes avec prédicats fermés est soluble en Temps Polynomial Non déterministe (NP) étant donné un oracle pour l'entailement partiellement fini.

5. Importance

• Pont entre théorie et pratique : Ce travail comble le fossé entre la richesse théorique des modèles infinis (nécessaire pour les logiques expressives) et les contraintes pratiques des domaines finis (nécessaires pour les applications de bases de données).
• Gestion des prédicats fermés : Les prédicats fermés (où l'extension d'un concept est connue et finie) sont cruciaux pour l'intégration de bases de données et la réponse aux requêtes médiatisée par des ontologies. Cet article fournit une fondation rigoureuse en théorie de la complexité pour le raisonnement avec eux dans des logiques expressives comme $\mathcal{S}$.
• Perspectives sur l'évolutivité : Le résultat de complexité (2-ExpTime) suggère que, bien que le problème soit difficile, il n'est pas indécidable, et que les bornes supérieures s'alignent avec les systèmes existants (comme SUMA) qui utilisent des stratégies de matérialisation partielle.
• Voies futures : Les auteurs suggèrent d'étendre ces techniques à d'autres logiques manquant de contrôlabilité finie (par exemple $\mathcal{ALCIF}$) et à d'autres tâches de raisonnement comme l'inclusion de requêtes et l'énumération.

En résumé, l'article établit avec succès que le raisonnement avec des contraintes « partiellement finies » est computationnellement faisable et fournit les mécanismes nécessaires en théorie des modèles pour gérer la divergence entre les modèles finis et infinis dans les Logiques de Description expressives.