Tuesday the 12th of July 2022
Optimised tableau algorithms for reasoning in the description logic ALC extended with link keys
Abstract:
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 that 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 algorithm, 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.
Mis à jour le 7 July 2022