Optimised tableau algorithms for reasoning in the description logic ALC extended with link keys

Les graphes de connaissances (KG) sont sans cesse utilisés par différentes organisations pour représenter des entités du monde réel sous la forme d’un graphe. Ils peuvent utiliser une couche ontologique pour décrire les classes et les propriétés des entités représentées. Les graphes de connaissances RDF sont des graphes de connaissances qui transmettent au modèle RDF. L’interconnexion des graphes de connaissances RDF consiste à identifier différents IRIs appartenant à différents graphes de connaissances RDF et faisant référence à la même entité du monde réel. Cela facilite l’intégration et l’interopérabilité des données en combinant différentes descriptions d’entités présentes dans différents graphes de connaissances.Il existe différentes méthodes pour aborder la tâche d’interconnexion des graphes de con- naissances RDF. Les clés de liage font partie de ces méthodes. Elles sont utilisées pour in- terconnecter des graphes de connaissances RDF décrits à l’aide de différentes ontologies. Les clés de liage spécifient les propriétés à comparer pour décider si deux entités appartenant à des classes différentes et présentes dans des graphes de connaissances différents sont les mêmes.Les clés de liage peuvent être exprimées sous forme d’axiomes logiques, et il est donc possible de les combiner avec des ontologies et des alignements d’ontologies pour effectuer un raisonnement logique. Dans cette thèse, nous avons pour objectif d’étudier le problème du raisonnement avec des clés de liages. Pour étudier formellement ce problème, nous modélisons les graphes de connaissances RDF, les ontologies et les alignements d’ontologies en utilisant la logique de description ALC. Nous choisissons la logique de description ALC comme langage de base pour le raisonnement. ALC couvre de nombreuses capacités de modélisation utilisées pour la représentation des connaissances et permet une extension plus facile à des logiques de description plus expressives. Nous étendons ALC avec des clés de liage et des égalités individuelles, la logique de description résultante est appelée ALC+LK. Nous montrons que l’implication des clés de liage peut être réduite à la vérification de la cohérence des clés de liage sans avoir besoin d’introduire la négation des clés de liage.Ensuite, nous concevons un algorithme pour décider de la cohérence de l’ontologie ALC+LK. Nous avons prouvé que l’algorithme est correct, complet et qu’il se termine toujours. Cet algorithme s’exécute en 2EXPTIME. Cependant, il existe des algorithmes EXPTIME pour raisonner en ALC et les règles de complétion ajoutées pour traiter les clés de liage et les égalités ne nécessitent pas plus de puissance de calcul que celle de ALC.À la lumière de ce qui précède, nous concevons un algorithme correct, complet et opti- mal dans le pire des cas pour le raisonnement en ALC+LK. Cet algorithme est inspiré de l’algorithme du tableau comprimé, qui permet d’obtenir le résultat de complexité optimale EXPTIME. Cependant, cet algorithme a un comportement non dirigé qui entrave son implé- mentation.Enfin et surtout, nous proposons un algorithme de tableau correct, complet et optimal dans le pire des cas pour le raisonnement dans la logique de description ALC avec des individus et des clés de liaison. Cet algorithme, contrairement à celui non dirigé, est dirigé par l’application de règles de complétion. Cela évite la génération de structures inutiles et facilite son implémentation. Nous implémentons cet algorithme et fournissons un certain nombre d’expériences de preuve de concept qui démontrent l’importance du raisonnement avec des clés de liage pour la tâche d’interconnexion des données.Knowledge Graphs (KGs) are unceasingly used by different organisation to represent real- world entities in the form of a graph. They may use an ontological layer for describing the classes and properties of the represented entities. RDF knowledge graphs are knowledge graphs that convey to the RDF model. RDF knowledge graph interlinking is the task of identifying different IRIs belonging to different RDF knowledge graphs and referring to the same real- world entity. This facilitates data integration and interoperability by combining different entity descriptions present in different knowledge graphs.There exist different methods for addressing the task of interlinking RDF knowledge graph. Link keys are among these methods. They are used for interlinking RDF knowledge graphs described using different ontologies. Link keys specify the properties to be compared to decide whether two entities belonging to different classes and present in different knowledge graphs are the same.Link keys can be expressed as logical axioms, and, thus, it is possible to combine them with ontologies, and ontology alignments to perform logical reasoning. In this thesis, we aim to study the problem of reasoning with link keys. To formally investigate this problem, we model RDF knowledge graphs, ontologies, and ontology alignments using the description logic ALC. We choose the description logic ALC as a base language for reasoning. ALC covers many modeling capabilities used for knowledge representation and allows for a more easy extension to more expressive description logics. We extend ALC with link keys and individual equalities, the resulting description logic is called ALC+LK. We show that link key entailment can be reduced to link key consistency checking without the need of introducing the negation of link keys.Then we design an algorithm for deciding the consistency of ALC+LK ontology. We have proved that the algorithm is sound, complete, and always terminates. This algorithm runs in 2EXPTIME. However, there exist EXPTIME algorithms for reasoning in ALC and the completion rules added for handling link keys and equalities require no more computational power than that of ALC.In the light of the above, we design a sound, complete, worst-case optimal algorithm for reasoning in ALC+LK. This algorithm is inspired by the compressed tableau algorithm, which allows obtaining the EXPTIME optimal complexity result. However, this algorithm has a non- directed behaviour which obstruct its implementation.Last but most importantly, we propose a sound, complete, and worst-case optimal tableau algorithm for reasoning in the description logic ALC with individuals and link keys. This al- gorithm, in contrast to the non-directed one, is directed by the application of completion rules. This avoids the generation of useless structures and facilitates its implementation. We implement this algorithm and provide a number of proof-of-concept experiments that demonstrates the importance of reasoning with link keys for the data interlinking task