In the field of knowledge representation and reasoning, description logics are commonly used to design knowledge bases and to reason about this knowledge. Various algorithms have been introduced to solve common reasoning problems, some of which compute models of the knowledge bases. There are, however, reasoning services that require models to admit certain properties not taken into consideration by these algorithms. This, for instance, is the case for explaining reasoning results using models. Consequently, our research goal is to identify desired model properties and to define appropriate model transformations as well as to investigate the computational complexity of these transformations.
Consequently, this project is concerned with the transformation of models of DL knowledge bases such that the resulting model satisfies additional properties, which depend on the use case. More precisely, we identify desired properties of models to, for instance, serve as explanation, and define according model transformations as well as investigate their computational complexity.
A main motivation for the manipulation of models of DL knowledge bases is, as mentioned before, explanation of reasoning results. Some reasoning results computed by DL systems can be far from obvious due to a number of reasons, e.g. because of the size and complexity of the respective knowledge base or because of a lack of familiarity with the logical syntax and deduction steps. There are, in principle, two ways of explaining reasoning results of DL systems for users. First, the reasoning result should be deducible in a logical calculus in case of positive entailment. This approach seems natural for positive entailments but less striking for explaining negative entailments. We take the path of explaining reasoning results semantically, which is the second way of explaining. This means we provide suitable models as prototypical examples to users in order to explain positive reasoning results, and we present suitable counter examples in case of negative reasoning results.
DL reasoner systems are optimized in terms of eficient computation of reasoning results. Hence, the computed models can appear artificial and counter-intuitive to users of DL systems. In order to make the reasoning result based on the computation of a model more comprehensible, the model can be transformed into another model of the DL knowledge base that admits additional properties, which shall foster human understanding of the reasoning result under consideration. For instance, possibly small models could ease comprehension since they do not contain redundancies. To identify interesting properties and discuss their meaning for improving model based explanations is part of this project. Besides, a mere visualization of the knowledge base by a well-shaped model can already help users to understand their knowledge base without having to read all its logical formulae, which already requires a certain level of expertise. Of course, one can transform models for various purposes other than to improve explainability. The need for transforming models becomes evident whenever a use case requires the model of the knowledge base to satisfy an additional property that is not expressible in the respective DL. For instance, the well-investigated DL ℒ, and hence any less expressive DL, admits the tree model property, intuitively meaning that no ℒ knowledge base (without constants) can enforce its models to be tree-shaped or prevent them from being tree-shaped because tree-shapedness is not expressible in ℒ. Hence, if the knowledge base is meant to model tree-shaped structures, such as pedigrees, transforming models into tree-shape while simultaneously maintaining their model property w.r.t. the given knowledge base can be useful.
In short, the general goal of this project is to define, investigate, and provide instances of a model transformation framework for specifying mappings over models of DL knowledge bases such that the images satisfy additional constraints while maintaining their model property.
In this framework, the desired property is a parameter, as is the respective knowledge base. This framework can then be used to define and discuss concrete instances of it as well as to classify model transformations w.r.t. the parameters of the framework.
This implies two aspects. First, the search for properties and use cases in which model transformations are useful. For these cases, we define appropriate transformations and prove their soundness. Second, the investigation of such framework w.r.t. general aspects, such as the computational complexity of model transformations given a certain logical language in which the desired model property is formalized. Such a language could be monadic second-order logic (MSO), or any other language that is more expressive than the DL in use.
The ideal of this research line would then be to construct an automated service for model transformations with user definable properties.
Explainabilty of logic-based AI reasoning is an active research area with various approaches,
see e.g. [
On the semantic side, there is previous work on making entailments more intelligible by revealing only parts of the respective model in a user interactive fashion [7]. Other approaches suggest visualizations of DL concepts by models, where information that is irrelevant to the user is filtered [ 8]. In addition, there is previous work on computing minimal models for FOL [9]. Nonetheless, to the best of our knowledge, there is little research about transforming DL models respecting user definable properties.
Since DL models can be regarded as edge and vertex-labeled graphs, the initial formalism of choice is MSO graph transductions [10], which is a powerful tool to specify maps over graph structures using MSO formulae with free variables. Since many DLs admit the finite model property, decidability of these MSO formulae is noncritical. The definition of our model transformation framework is, however, not limited to MSO graph transductions. A well known alternative are, for instance, Graph Rewriting Systems [11].
In [12], we present a model transformation framework as described in Section 3 and define the basic decision problem of a successful transformation, meaning that a model transformation as an instance of the framework is called successful if and only if the image of the model transformation is indeed a model of the respective knowledge base that satisfies the additionally desired property. As an example instance of this framework, we construct a family of transformations for the DL ℒ for obtaining finite tree-like models. We call the transformations ℓ-unraveling, where ℓ is an integer determining the depth of the unraveling, and prove that they are model-preserving by showing that any model and the transformations of it are bisimilar.
We provide another use case of model transformations in [13, 14, 15], where models are transformed in order to explain non-entailment for the DL ℰℒ. The objective is to reduce counter examples for the non-entailment in question to a relevant minimum. Lastly, in a use case that does not have explanation as focus, we apply the model transformation techniques in [16] for repairing ℰℒ knowledge bases using methods from formal concept analysis [17].
The first line of research is the extension of the catalogue of interesting properties for models that foster human understanding of knowledge bases and reasoning results. To support users of DL systems, findings from cognition theory are to be taken into consideration. Furthermore, user studies can be conducted to empirically verify the suitability of potentially interesting model properties.
The second direction of research is dedicated to the further investigation of the model transformation framework introduced in [12]. An open question in this context is if there can be an automated reasoning service that allows a user to specify a desired property for a model of a given knowledge base and deduces the MSO formulae that define the MSO transduction needed to transform the respective model. Future work can also consider model transformations with constants to incorporate reasoning services using named elements — foremost query answering over TBox and ABox. Since there are multiple formalisms to define model transformations, it appears also reasonable to compare these formalisms with respect to their suitability for the overall task by, for instance, investigating their expressive power.
This work has been supported by DFG in RTG 1763. [6] C. Alrabbaa, F. Baader, S. Borgwardt, P. Koopmann, A. Kovtunova, Finding small proofs for description logic entailments: Theory and practice, in: E. Albert, L. Kovacs (Eds.), Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2020), volume 73 of EPiC Series in Computing, EasyChair, 2020, pp. 32–67. [7] J. Bauer, U. Sattler, B. Parsia, Explaining by example: Model exploration for ontology comprehension, in: B. C. Grau, I. Horrocks, B. Motik, U. Sattler (Eds.), Proceedings of the 22nd International Workshop on Description Logics, volume 477 of CEUR Workshop Proceedings, CEUR-WS.org, 2009. [8] F. N. do Amaral, C. B. Martins, Visualization of description logic models, in: F. Baader, C. Lutz, B. Motik (Eds.), Proceedings of the 21st International Workshop on Description Logics, volume 353 of CEUR Workshop Proceedings, CEUR-WS.org, 2008. [9] P. Baumgartner, A. Fuchs, H. De Nivelle, C. Tinelli, Computing finite models by reduction to function-free clause logic, Applied Logic 7 (2009) 58–74. [10] B. Courcelle, J. Engelfriet, Graph Structure and Monadic Second-Order Logic, volume 138 of Encyclopedia of Mathematics and its Applications, Cambridge University Press, 2012. [11] R. Heckel, Graph transformation in a nutshell, Electronic Notes in Theoretical Computer
Science 148 (2006) 187–198. [12] W. Hieke, A.-Y. Turhan, Towards model transformation in description logics — Investigating the case of transductions, in: C. Beierle, M. Ragni, F. Stolzenburg, M. Thimm (Eds.), Proceedings of the 6th Workshop on Formal and Cognitive Reasoning, volume 2680 of CEUR Workshop Proceedings, CEUR-WS.org, 2020, pp. 69–82. [13] C. Alrabbaa, W. Hieke, A.-Y. Turhan, Counter model transformation for explaining nonsubsumption in ℰℒ, in: C. Beierle, M. Ragni, F. Stolzenburg, M. Thimm (Eds.), Proceedings of the 7th Workshop on Formal and Cognitive Reasoning, volume 2961 of CEUR Workshop Proceedings, CEUR-WS.org, 2021, pp. 9–22. [14] C. Alrabbaa, W. Hieke, A.-Y. Turhan, Relevant parts of counter models as explanations for ℰℒ non-subsumptions (extended abstract), in: Informal Proceedings of the 2nd Workshop on Explainable Logic-Based Knowledge Representation, 2021. [15] C. Alrabbaa, W. Hieke, Explaining non-entailment by model transformation for the description logic EL, in: A. Artale, D. Calvanese, H. Wang, X. Zhang (Eds.), Proceedings of the 11th International Joint Conference on Knowledge Graphs (IJCKG 2022), Association for Computing Machinery (ACM), 2022, pp. 1–9. [16] W. Hieke, F. Kriegel, A. Nuradiansyah, Repairing ℰℒ TBoxes by means of countermodels obtained by model transformation, in: M. Homola, V. Ryzhikov, R. A. Schmidt (Eds.), Proceedings of the 34th International Workshop on Description Logics, volume 2954 of CEUR Workshop Proceedings, CEUR-WS.org, 2021. [17] F. Kriegel, Constructing and Extending Description Logic Ontologies Using Methods of Formal Concept Analysis, Ph.D. thesis, TU Dresden, 2019.