Models for Description Logic (DL) ontologies can be used for explanation purposes, but the models computed by standard DL reasoner systems are not necessarily suitable for this task. In this paper we investigate the general task of transforming an arbitrary model into a target model that admits the desired property. To this end, we introduce a general framework for model transformation that abstracts from the DL in use, the property of the target model and the transformation formalism. We consider instantiations of the framework for the DLs ALC and EL and use transductions as transformation formalism.
Description Logics (DLs) are a family of knowledge representation languages that are widely used in ontology-based applications. Most DLs are fragments of firstorder logic (FOL) that have decidable reasoning problems. Ontologies usually capture definitions for terminologies from an application domain by concept axioms. These axioms can refer to other concepts or roles, which are unary and binary predicates, respectively.
DL ontologies can easily grow very large and complex and thus, a
consequence computed by a DL reasoner is not necessarily obvious for a knowledge
engineer and automated ontology services to explain the results of reasoning are
needed. Such a service is the computation of justifications and was intensively
investigated in recent years, see [
For a range of DLs there are highly-optimized reasoner systems available
such as FaCT++ [
As classical DLs use only unary predicates and binary relations, their models are node and edge labeled graphs and can be easily be depicted. For a graphical representation of a concept instance, it could be advantageous, if the model was for instance small, or tree-like, or planar, and so on. We consider these properties here—not so much to argue for their cognitive adequateness for explanation, but rather to illustrate by their use that our approach can handle properties that can reasonably be required for these purposes. We address the task of model transformation by introducing a framework, in which the intended property to be satisfied by the model is kept variable. This allows for different properties depending on the application. We introduce a general framework for transforming arbitrary models of ontologies. This framework is subsequently used to formalize reasoning problems and to investigate a prominent one in depth in this paper.
As the formalisms for transformations, we use transductions (as defined in
[
As a concrete instantiation of our framework, we investigate the case of transforming arbitrary models of ontologies written in the DL called ALC into a tree(-like) models by transductions. We construct a family of transductions over interpretations and show that these transformations are model preserving, i.e. input and output model satisfy the same sentences in the DL ALC. We also briefly consider a lightweight DL that is of limited expressiveness, but has good computational properties and has the canonical model property (sometimes called universal model). The canonical model would allow for imposing assumptions on the model that is to be transformed.
This paper is structured as follows: in Section 2, we define the basic notions of DL and transductions. We define the model transformation framework and dedicated reasoning problems for it in Section 3 and consider the case of transductions to tree-like models in Section 4 as an instantiation of our framework for ALC knowledge bases. We also discuss aspects of model transformation for EL. Last, we draw conclusions and lay out future work in Section 5. 2
As this paper mainly combines notions from Description Logics and graph
transductions, we briefly introduce the main notions from these fields. For detailed
introductions, see [
Description Logics The main building blocks for DL knowledge bases are concepts, which describe unary predicates from the modeled domain. We use sets for concept names NC and for role names NR. Let A ∈ NC and r ∈ NR, then complex ALC concepts can be built according to the following grammar:
C := A | > | ¬C | C u C | ∃r.C .
Commonly used abbreviations are: C1 t C2 := ¬(¬C1 u ¬C2), ⊥ := ¬>, and ∀r.C := ¬(∃r.¬C). The semantics is defined as in first-order logic by means of interpretations, which are a tuple I = (ΔI , ·I ), consisting of the domain ΔI and a function ·I that maps elements from NC to subsets of the domain and elements from NR to subsets over ΔI × ΔI . The mapping ·I is extended to (complex) ALC concept descriptions as follows: >I = ΔI , ¬CI = ΔI \ CI , (C1 u C2)I = C1I u C2I and (∃r.C)I = {d ∈ ΔI | ∃e.(d, e) ∈ rI and e ∈ CI }. The fragment of ALC that only uses the top-concept >, conjunction (u), and existential restrictions (∃r.C) as concept constructors is called EL. Note that EL cannot express inconsistencies.
Terminological knowledge about the application domain can be modeled by using (complex) concept descriptions. Let C and D be concepts, a general concept inclusion (GCI) is a statement of the form: C v D. A TBox T is a finite set of GCIs. An interpretation I satisfies a GCI C v D, if CI ⊆ DI . An interpretation I is a model of a TBox (I |= T ) if and only if I satisfies C v D for all C v D ∈ T . A knowledge base K is a pair of a TBox T and an ABox A. The latter can express knowledge about objects by the use of constants. We concentrate on terminological knowledge and do not introduce ABoxes formally. We assume A to be empty in K. We denote by Σ(I) the signature of I, i.e., the set of concept and role names occurring in I; and for concepts C and GCIs, respectively. We write ΣA := Σ ∩ NC and Σr := Σ ∩ NR and we assume signatures to be finite.
Typical reasoning problems for DLs are to decide satisfiability and subsumption. Satisfiability checks for the existence of a model for a given concept or TBox and subsumption checks for super-concept relationships between two given concepts w.r.t. a TBox and is formally defined as: D subsumes C w.r.t. TBox T (written C vT D) iff in all models I of T holds: CI ⊆ DI .
DLs differ in their expressivity and this often shows in the complexity for
reasoning. For ALC, testing subsumption of concepts w.r.t. a non-empty TBox
is ExpTime-complete [
Transductions We now define transductions in regard to DL interpretations. Observe that such an interpretation is effectively a directed graph with labeled vertices (indicating concept membership) and labeled edges (indicating membership to a role). Intuitively in a transduction, vertices and edges from one interpretation are being copied into a new interpretation if they satisfy a condition given by a logical formula. Depending on the fulfillment of the conditions, the new copy can be modified. If the conditions are formulated in monadic second-order logic (MSO) or FOL, we call the transduction a MSO- or FOL-transduction, respectively.
Since typical DL interpretations have at most binary predicates, we restrict
the standard definition of transductions of relational structures from [
Let Σ and Σ0 for the remainder of this paper be binary signatures. A transduction τ of type from Σ to Σ0 is a binary relation on Σ-interpretations or formally, τ ⊆ I(Σ) × I(Σ0). We call the input of a transduction source interpretation and its output target interpretation. The logical formulae that capture the transformation conditions and thereby induce a particular transduction are comprised in a tuple called definition scheme.
Definition 1 (Definition scheme). Let Par be a finite set of variables called
parameters. Let AuxVar be a finite set of variables called auxiliary variables s.t.
Par ∩ AuxVar = ∅, let x, y ∈ AuxVar, and L be a logic. A definition scheme of
type from Σ to Σ0 with set of parameters Par is a tuple of formulae of the form
D = (χ, (δi)i∈[k], (θω)ω∈(ΣA0×[k]), (ηω)ω∈(Σr0×[k]2))
for some k ∈ N+ (we call positive integers N+ index set and abbreviate {1, . . . , k}
with [k]), where
– χ ∈ L(Σ, Par) is the precondition;
– δi ∈ L(Σ, Par ∪ {x}) for each i ∈ [k] are domain formulae;
– θω ∈ L(Σ, Par ∪ {x}) for each ω ∈ ΣA0 × [k], and are concept formulae; and
– ηω ∈ L(Σ, Par ∪ {x, y}) for each ω ∈ Σr0 × [k]2 are the role formulae.
A definition scheme D is an L-definition scheme, if all its formulae are written
in some logic L. If Par = ∅ for D, then D is called parameterless.
Please note that a definition scheme is also called a graph transducer in [
Next, we define how a target interpretation is induced by a definition scheme from a source interpretation I. If applied to sets of interpretations and parameter assignments, this method then gives rise to a transduction.
Definition 2 (Transduction induced by a definition scheme). Let I = (ΔI , ·I ) be a Σ-interpretation, λPar : Par → ΔI , be a parameter assignment, and
D = (χ, (δi)i∈[k], (θω)ω∈(ΣA×[k]), (ηω)ω∈(Σr×[k]2)) a definition scheme. Let λ be the assignment that extends λPar s.t. λ(x) = a and (I, λPar) |= δi(a) stand for (I, λ) |= δi (and extending it accordingly for the θi and ηi). Then I0 is the Σ0-interpretation defined by D from (I, λPar) iff: – (I, λPar) |= χ, – ΔI0 := {(a, i) ∈ ΔI × [k] | (I, λPar) |= δi(a)}, – AI0 := {(a, i) ∈ ΔI0 | (I, λPar) |= θω(a)} for all A ∈ ΣA(I), and – rI0 := {((a1, i1), (a2, i2)) ∈ (ΔI0 × ΔI0 ) | (I, λPar) |= ηω(a1, a2)} for all r ∈ Σr(I).
As the interpretation I0 is uniquely determined by D, I, and λ iff (I, λ) |= χ, we obtain the transduction τD induced by D and use the function τD(I, λ) = I0 directly.
Note that transductions, as in [
To be able to investigate model transformations in a wider setting in a structured and well-defined way, we define a general framework that abstracts from the concrete property to be achieved for the target interpretation, the knowledge base, and even the logics employed. The parameters of the framework are, the knowledge base K under consideration together with an interpretation I over the same signature. We write LK for the logic in which the knowledge base is formulated. The desired property is a sentence ρ of some logic Lρ. We sometimes write ρ-model for a model that satisfies property ρ. Another parameter is the actual transformation mapping. As we concentrate on transductions, we use τ to transform arbitrary source models of K to desired ρ-models.
Definition 3 (Model transformation framework). Let LK be a description logic, K an LK-knowledge base, I an interpretation over the signature Σ(K), ρ a sentence formulated in some logic Lρ and τ : I(Σ(K)) → I(Σ(K)) a transformation mapping over interpretations of the binary signature Σ(K). We call S = (I, K) the source pair and T = (ρ, τ ) the transformation pair. We use transductions to describe model transformations and restrict ourselves to empty ABoxes and finite interpretations. In principle, the framework would also allow for other kinds of transformations or even structures of higher arity. The main reasoning tasks using the framework is to decide if a transformation pair applied to a source pair is successful.
Definition 4 (Successfulness problems). Let S = (I, K) be a source pair and T = (ρ, τ ) be a transformation pair. Let LK be a DL. A pair (S, T ), is called successful, denoted by successful(S, T ), iff I |= K implies τ (I) |= K ∪ {ρ}. – The successfulness problem for S and T is to decide for a given (S, T ) with
S = (I, K) and T = (ρ, τ ), whether (S, T ) is successful. – The successfulness problem for a DL and a transformation pair is to decide for a given DL LK and T = (ρ, τ ), whether for every S = (I, K), where K is expressed in LK, the pair (S, T ) is successful.
Please note that, in case I 6|= K, the success of a pair (S, T ) is trivially given. Furthermore, K and ρ can be inconsistent, meaning that there is simply no model for K ∪ ρ. Thus the successfulness property does not hold trivially in every case.
In principle the framework can easily give rise to other reasoning problems. An interesting question that generalizes the successfulness problem is whether for a given DL LK and a given property ρ, a LK-KB has a ρ-model. Definition 5 (ρ-model existence problems). Given a DL LK and a property ρ formulated in a logic Lρ.
– The ρ-model existence problem for K decides whether there exists a ρ-model for a given KB K formulated in LK. – The ρ-model existence problem for LK decides whether there exists a ρ-model for every consistent KB K formulated in LK. To answer these question may necessitate to compare the expressiveness of LK and the logic Lρ that ρ is formulated in. To decide the ρ-model existence problem for a given KB K where Lρ is not more expressive than LK, the condition to fulfill the property ρ can, in principle be answered by employing the DL reasoner for LK. For some cases, the ρ-model existence problem for a DL LK is already answered. For instance, in case of the existence of tree-shaped models, these do always exist for ALC concepts defined w.r.t. a TBox, because ALC has the tree model property, i.e. any ALC concept satisfiable w.r.t. a TBox also has a model that is tree-shaped.
We focus in this paper on the successfulness problem for a DL and a transformation pair, i.e. we want to obtain general results of the form: given a transformation pair T , for all source pairs S of a given DL LK, successful(S, T ) holds. This is the case if τ is a model preserving relation w.r.t. a logic LK. For instance, by the virtue of invariance results it holds that, if source and target interpretation of τ are proven to be globally (ALC)-bisimilar, every (ALC) knowledge base satisfied by the source interpretation is also satisfied by the target one.
Ultimately, it would be desirable to not only decide successfulness, but to compute the actual ρ-model for a source pair. Given a particular ρ, it is not obvious how to obtain a suitable definition scheme. For instance, if ρ requires the model to have no isolated vertices, the scheme could either connect or delete those vertices from the input model. So it is not trivial to derive the formulae for the definition scheme merely from the property ρ for the target model. We are interested in the investigation of the relation of ρ to the formulae of a definition scheme for future work. 4
We introduce a family of transductions (τ`-Tree)`∈N as transformation formalism for source pairs S = (I, K), where K is an ALC knowledge base (with an empty ABox). The goal is to achieve a tree(-like) model which is defined as follows. Definition 6 (Property `-tree-like). A pointed interpretation (I, d) satisfies the property `-tree-like iff it is one connected component and a partitioning of the edges into 3 sets s.t.
– d has no predecessor w.r.t. the first partition of the edges and for every element that is reachable from d by a non-empty path of length < ` by edges of that partition there is only one predecessor, – each element e that is reachable from d by a path of length ` is a node in a directed graph Ge, whose edges belong exclusively to the second partition and each directed graph Ge has at most one node reachable from d by a path of length ` – edges in the third partition exclusively have their first component in the directed graph Ge and their second component in the path from d to e. Intuitively, we want to unravel arbitrary models for ALC KBs into a tree of (user definable) depth `. The DL ALC admits the tree model property as well as the finite model property, but need not have finite tree models. Hence, some leaves of the tree might need to re-use elements as successors, since the transformation must be model preserving. The idea is to introduce back-loops to the branches of the tree to the most recent suitable ancestor. The resulting model is `-tree-like. As an intuitive example consider the TBox {A v ∃r.A} and the interpretation I = ({a}, {(a, a) ∈ r}). Our transformation would create an ` long chain of copies of a connected by an r-edge and needs to loop back to some element.
The idea for the unraveling transduction is the following. The “root” element
d is copied into the domain of the target interpretation I0 and is the root of the
tree-like interpretation. As in the standard tree-unraveling defined for
interpretations (see [
We use the following auxiliary predicate to express reachability (confer [
D`-Tree = χ, (δw)w∈α(I,`), (θC,w)C∈ΣA,w∈α(I,`), (ηr,(w,w0))r∈Σr,(w,w0)∈α(I,`)2 , where the components are defined as follows: – Precondition: χ(y) := ∀x : x 6= y → reach(x, y) (2) – Domain formulae are defined by means of the following formulae: δroot(y, u) := u = y w
|w| δinner(y, u) := ^ w
_ r(xi, xi+1) ∧ (x1 = y) ∧ (x|w|+1 = u) i=1 r∈Σr δleaf (y, u) := δw0 (y, x|w|) ∧ reach(x|w|, u) ∧ w δwroot(y, u) , if |w| = 0 δw(y, u) := δwinner(y, u) , if |w| ≤ ` − 1 δwleaf (y, u) , if |w| = ` & w = w0 · x` |w| ^ u 6= xi i=1 The variable xi used in the formulae of D`-Tree needs to be mapped by λ to the according xi ∈ w.1 – Concept name formulae: θA,w(u) := A(u) – Role name formulae: ηr,(w,w0) are defined by means of the following formulae: ηrth,(icwk,ewt0)(u, v) := r(u, v) ηrb,r(awnc,hw0)(u, v) := r(u, v) ∧ w0 = w · u
m ηrb,a(cwk-,wlo0o)p(u, v) := r(u, v) ∧ ^ xi = yi ∧ i=1 n ^ i=m+1
xi 6= v ηrth,(icwk,ewt0)(u, v) ηr,(w,w0) := ηrb,r(awnc,hw0)(u, v) if |w| = |w0| = ` if |w0| = |w| + 1 & |w0| < ` ηrb,a(cwk-,wlo0o)p(u, v) if |w0| < |w| & |w| = ` The definition schema D`-Tree together with the assignment λPar : y 7→ d, then defines the transduction relation τ`. Other (undefined) cases are set to the Boolean constant ⊥.
Note that the index set is not the natural numbers, but the set of words over ΔI up to length `. This is w.l.o.g. as there always is an order on that index set isomorphic to the natural numbers, e.g. the lexicographic order. According to Definition 2, every transduction induced by a definition scheme can only increase the domain size linearly. Using α(I, `) as index set, however, the increase of the domain size is limited to |ΔI | · |α(I, `)|, and |α(I, `)| = P`k=1 |ΔI |k, which is not linear but still polynomial. 1 This is an element in ΔI by definition, i.e. the transduction uses more parameters than just the unraveling node d. For eased readability we use xi for both the variable in the formulae and the domain elements of I since we identify them with λ. (4) (5) (6) (7) (8) (9) (10) (11) Butterfly b
ult-form s-ad a h
spring s-off a h eats a
We before we investigate formal properties of the unravelling transduction, we illustrate the unraveling of a model of TK by an example in the realm of biology. Consider the following TBox that speaks about caterpillars, butterflies and plants. It states that all butterflies eat plants and have caterpillars as offspring. Also, every caterpillar eats plants and has a butterfly as an adult form. Lastly, every plant has a plant as offspring.
Tex := { Butterfly v (∃has-offspring.Caterpillar) u (∃eats.Plant),
Figure 1 depicts a model Iex for the TBox Tex using only three domain elements.
Concept names are written next to the nodes and the labeled arrows depict roles.
Such a succinct model could be the outcome of the reasoning process of reasoners
that aim at keeping the domain of the model small by eagerly reusing domain
elements and blocking the introduction of new elements possible—a strategy
known as anywhere blocking that is implemented by the HermiT reasoner [
Model Iex, however, has some shortcomings when it comes to explaining the concepts under consideration. For instance, the offspring of a butterfly is certainly not the caterpillar that this butterfly developed from. Also, a regular plant not its own offspring. A model unraveling might help to resolve some of these artifacts due to reasoner optimization.
Figure 2 shows the 2-unraveling of IK . The parts of the unraveled model in solid lines highlight the tree of depth 2 and the dotted lines and are being added for the transformation to be model preserving. In the part of the model drawn in solid lines, we now have that the offspring of a butterfly is no longer the caterpillar it emerged from and also, plants have other (freshly introduced) plants as offspring, too. For explanation purposes, users might only be interested in the non-dotted part and an implementation could simply omit the parts drawn in dotted line if the user permits.
We show now that the unraveling transduction is successful for all ALC KBs. To this end we employ bisimulations between source and target interpretations. Lemma 1. The relation ' := {(x, (x0, w)) | (x0, w) ∈ Δτ`-Tree(I) & x = x0}) is a bisimulation between I and τ`-Tree(I). Caterpillar
Butterfly has-adult-form
has-offspring aab eats ba
Caterpillar has-adult-form aε
eats eats
has-offspring has-offspring caba Plant ca
Plant has-offspring
has-offspring cab
Plant cac
Plant
Proof. We denote τ`-Tree(I) by I0. Since x0 in (x0, w) ∈ ΔI0 is an element of ΔI , we can state x = x0 as condition. Assume I |= χ, so that τ`-Tree(I) is defined. We need to show three conditions for this claim.
First, x ' (x0, w) implies x ∈ AI ⇔ (x0, w) ∈ AI0 for all x ∈ ΔI , (x0, w) ∈ ΔI0 and A ∈ ΣA; this condition follows directly from concept name formula (7).
Second, x ' (x0, w) and (x, y) ∈ rI implies the existence of (y0, w0) such that ((x0, w), (y0, w0)) ∈ rI0 and y ' (y0, w) for all x, y ∈ ΔI , (x0, w), (y0, w0) ∈ ΔI0 and all r ∈ Σr. Assume (x, y) ∈ rI and x ' (x0, w). Since I satisfies the precondition (2), there is a path in I from the unraveling node d to x and hence to y. Now, domain formulae (3) and (4) create a fresh copy for each element ending in a d-path in I up to length `. If the path from d to x is of length at most ` in I, we have to distinguish two cases, because an r-successor could have been copied before in this path. If the r-successor has been copied before, domain formula (4) is true for y and is hence copied into the domain of I0, i.e. there is an (y, w) ∈ ΔI0 . If the r-successor y of x in I has not been copied yet (because the d-path is longer than `), domain formula (5) is true for y and hence y is copied into the domain of I0 as well. To see that the role relationships are set correctly, we consider two cases. The considered path from d to y over x in I is of length up to ` or it is not. Role formula (9) connects two nodes (x, w) and (y, w0) with an redge if r(x, y) holds in I and w = w · x. In the latter case, we again distinguish two cases. If the r-successor y of x in I is already reachable over a prefix of path of (x, w), then (10) adds the redge to an earlier copy of y in I0. If there is no copy of a prefix of w, relation formula (8) connects (x0, w0) and (y0, w0) whenever x is connected to y in I.
Third, x ' (x, w) and ((x0, w), (y0, w0)) ∈ rI0 implies the existence of y ∈ ΔI such that: (x, y) ∈ rI and y ' (y0, w0) for all x ∈ ΔI , x0, y0 ∈ ΔI0 and r ∈ Σr. Similarly to the previous argument, assume we are given (x ' (x0, w) and (x0, y0) ∈ rI0 . Then, there is a path in I0 from d over x to y, since y0 is copied if and only if there is such a path according to domain formulae (4) and (5). And here as well as in the previous condition, an r-edge between (x, w) and (y, w) is added if and only if there is an r-edge between x and y in I.
Lemma 2. Let the set C := {[(x, w)]≡} of equivalence classes be defined by the equivalence relation (x, w) ≡ (x0, w0) iff x = x0 over Δτ`-Tree(I). Then C is a partitioning of the domain of τ`-Tree(I).
Corollary 1. Let I be an interpretation and τ`-Tree the unraveling transduction for some ` ∈ N. Then, if τ`-Tree(I) is defined, I and τ`-Tree(I) are globally bisimilar.
Proof. Recall the relation ' from Lemma 1. We show that for each e ∈ ΔI , there is an element e0 ∈ Δτ`-Tree(I), such that (I, e) ' (τ`-Tree(I), e0), and vice versa. To achieve this, we use the partitioning C from Lemma 2. For each element in the domain of I exists exactly one corresponding element in C. Following the argument in Lemma 1 and since τ`-Tree(I) is defined, for each reachable element from the unraveling node, there is at least one copy. Hence, the relation ' is a bijection between I and I0 and hence, we have that C is a partitioning. We also have that for each representative (e, w) of [(e, w)]≡, it is the case that e ' (e, w) as defined and hence we have that ' is global. So, we have that for each elements of the domains of I and I0, there is at least one bisimilar element in the other one respectively.
Theorem 1. For all source pairs S = (I, T ), where T is an ALC-TBox and I an interpretation holds: if τ`-Tree(I) is defined, then successful(S, T ). Proof. Direct consequence of Corollary 1 and Definition 6.
Note that the computational complexity of applying τ`-Tree to an input interpretation is the sum of evaluating the definition scheme over this interpretation. The amount of formulae to evaluate for τ`-Tree is polynomial in size of |ΔI | as mentioned before. To compute reachability (here expressed by the predicate reach(x, y)), well-known PTime time algorithms exist.
Considerations on model transformation for EL. Since the DL EL does
not use negation, every EL-KB has a model. A GCI formulated in EL is satisfied
in one interpretation I is also satisfied in another interpretation I’ iff there is
a homomorphism h : I 7→ I0. This seems clear from the fact that
homomorphisms are relation preserving mappings. Hence, if we instantiate our framework
such that LK = EL, we need to show that τ is a homomorphism in order to
guarantee successfulness for each EL TBox. As global bisimulation implies the
existence of a homomorphism, the τ`-Tree transduction preserves models of EL
knowledge bases. An important difference to ALC is that EL has the canonical
model property, which means that there always exists a model that can
homomorphically be embedded into any other model of the same EL-knowledge base.
Canonical models are the basis for reasoning in EL and they are computed by
all dedicated EL reasoners such as ELK [
We have defined and discussed a general framework for model transformation in DL—motivated by the task to generate models of DL TBoxes that are suitable for explanation. Based on this framework we have formally defined a collection of reasoning problems. By means of results from model theory one can address some of these reasoning problems. We have defined and investigated an `-tree unraveling of (finite) interpretations as a concrete instantiation of the framework and have shown that the corresponding transduction is model preserving with respect to any TBox formulated in the logic ALC.
In this paper we have mainly discussed the decision problems related to the existence of ρ-models. For the application of generating models that facilitate explanations, the corresponding computation problems are clearly of bigger interest as they pave the way to automatic support. However, it is not obvious how to use a property ρ to derive a suitable definition scheme for that property. In practice it would probably suffice to offer a fixed catalog of properties to a user in order to display a model with one or even several of the properties from the catalog. Having a catalog of properties for which there are definition schemes and results like Theorem 1 (with respect to a given logic), the transformations could be implemented in a tool, in which the user specifies the source and transformations pairs. Populating such a catalog with suitable model properties should be done in regard of results from the fields of cognitive sciences or visualization.
There are many extensions of this initial work to be studied in future work. An obvious extension of the work presented here, is to use ABoxes as well when computing or transforming models. As ABoxes add named individuals to models, transformations have to obey the unique name assumption, which says that differently named objects have to be mapped to different domain elements in interpretations. This assumption must not be violated by transformations.
The framework is not tied to transductions and as an alternative transformation formalism, graph rewriting systems are a interesting option. A comparison of graph rewriting systems and graph transductions in regard of treating models derived from DL knowledge bases is future work, as well. Acknowledgments. We would like to thank Heiko Vogler and the anonymous reviewers for their detailed and helpful remarks.